cases le_total a b <;> simp only [uIcc_of_le, uIcc_of_ge, *] at h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (uIcc a b)
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
case inl
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h✝ : a ≤ b
h : ContDiffOn ℝ 1 f (Icc a b)
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a

case inr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h✝ : b ≤ a
h : ContDiffOn ℝ 1 f (Icc b a)
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a