Theorem: ContDiffOn.integral_eq_sub_u (RMT4/to_mathlib.lean)

State before:
𝕜 : 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
Tactic:
cases le_total a b <;> simp only [uIcc_of_le, uIcc_of_ge, *] at h
State after:
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

State before:
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
Tactic:
simp [integral_eq_sub''', *]
State after:
no goals

State before:
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
Tactic:
simp [integral_symm b a, integral_eq_sub''', *]
State after:
no goals