Theorem: ContDiffOn.integral_eq_sub''' (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 (Icc a b)
hab : a ≤ b
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
Tactic:
convert h.integral_eq_sub hab using 1
State after:
case h.e'_2
𝕜 : 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 (Icc a b)
hab : a ≤ b
⊢ ∫ (y : ℝ) in a..b, deriv f y = ∫ (y : ℝ) in a..b, derivWithin f (Icc a b) y

State before:
case h.e'_2
𝕜 : 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 (Icc a b)
hab : a ≤ b
⊢ ∫ (y : ℝ) in a..b, deriv f y = ∫ (y : ℝ) in a..b, derivWithin f (Icc a b) y
Tactic:
apply integral_congr_uIoo
State after:
case h.e'_2.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 (Icc a b)
hab : a ≤ b
⊢ EqOn (fun t => deriv f t) (fun t => derivWithin f (Icc a b) t) (uIoo a b)

State before:
case h.e'_2.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 (Icc a b)
hab : a ≤ b
⊢ EqOn (fun t => deriv f t) (fun t => derivWithin f (Icc a b) t) (uIoo a b)
Tactic:
intro t ht
State after:
case h.e'_2.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 (Icc a b)
hab : a ≤ b
t : ℝ
ht : t ∈ uIoo a b
⊢ (fun t => deriv f t) t = (fun t => derivWithin f (Icc a b) t) t

State before:
case h.e'_2.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 (Icc a b)
hab : a ≤ b
t : ℝ
ht : t ∈ uIoo a b
⊢ (fun t => deriv f t) t = (fun t => derivWithin f (Icc a b) t) t
Tactic:
convert (derivWithin_of_mem_uIoo ht).symm using 3
State after:
case h.e'_3.h.e.h.e'_7
𝕜 : 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 (Icc a b)
hab : a ≤ b
t : ℝ
ht : t ∈ uIoo a b
⊢ Icc a b = uIcc a b

State before:
case h.e'_3.h.e.h.e'_7
𝕜 : 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 (Icc a b)
hab : a ≤ b
t : ℝ
ht : t ∈ uIoo a b
⊢ Icc a b = uIcc a b
Tactic:
simp [uIcc, hab]
State after:
no goals