Theorem: ContDiffOn.integral_derivWithin_smul_comp (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 : ℝ → ℝ
hg : ContDiffOn ℝ 1 g (uIcc a b)
hf : ContinuousOn f (g '' uIcc a b)
⊢ ∫ (x : ℝ) in a..b, derivWithin g (uIcc a b) x • (f ∘ g) x = ∫ (x : ℝ) in g a..g b, f x
Tactic:
refine integral_comp_smul_deriv'' hg.continuousOn (λ t ht => ?_) (hg.continuousOn_derivWithin'' le_rfl) hf
State after:
𝕜 : 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 : ℝ → ℝ
hg : ContDiffOn ℝ 1 g (uIcc a b)
hf : ContinuousOn f (g '' uIcc a b)
t : ℝ
ht : t ∈ Ioo (min a b) (max a b)
⊢ HasDerivWithinAt g (derivWithin g (uIcc a b) t) (Ioi t) t

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 : ℝ → ℝ
hg : ContDiffOn ℝ 1 g (uIcc a b)
hf : ContinuousOn f (g '' uIcc a b)
t : ℝ
ht : t ∈ Ioo (min a b) (max a b)
⊢ HasDerivWithinAt g (derivWithin g (uIcc a b) t) (Ioi t) t
Tactic:
apply (hg.differentiableOn le_rfl t (uIoo_subset_uIcc ht)).hasDerivWithinAt.mono_of_mem
State after:
𝕜 : 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 : ℝ → ℝ
hg : ContDiffOn ℝ 1 g (uIcc a b)
hf : ContinuousOn f (g '' uIcc a b)
t : ℝ
ht : t ∈ Ioo (min a b) (max a b)
⊢ uIcc a b ∈ 𝓝[>] t

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 : ℝ → ℝ
hg : ContDiffOn ℝ 1 g (uIcc a b)
hf : ContinuousOn f (g '' uIcc a b)
t : ℝ
ht : t ∈ Ioo (min a b) (max a b)
⊢ uIcc a b ∈ 𝓝[>] t
Tactic:
exact uIcc_mem_nhds_within ht
State after:
no goals