ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) = ∫ (u : ℝ) in f a..f b, g u
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntegrableOn g (f '' [[a, b]])
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) = ∫ (u : ℝ) in f a..f b, g u
rw [hf.image_uIcc, ← intervalIntegrable_iff'] at hg1
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
h_der :
  ∀ (x : ℝ),
    x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
⊢ (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) = ∫ (u : ℝ) in f a..f b, g u
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
⊢ (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) = ∫ (u : ℝ) in f a..f b, g u
have h_der :
  ∀ x ∈ Ioo (min a b) (max a b),
    HasDerivWithinAt (fun u => ∫ t in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x := by
  intro x hx
  obtain ⟨c, hc⟩ := nonempty_Ioo.mpr hx.1
  obtain ⟨d, hd⟩ := nonempty_Ioo.mpr hx.2
  have cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b) := by
    rw [uIcc_of_le (hc.2.trans hd.1).le]
    exact Icc_subset_Ioo hc.1 hd.2
  replace hg_cont := hg_cont.mono (image_subset f cdsub)
  let J := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
  have hJ : f '' [[c, d]] = J := (hf.mono (cdsub.trans Ioo_subset_Icc_self)).image_uIcc
  rw [hJ] at hg_cont
  have h2x : f x ∈ J := by rw [← hJ]; exact mem_image_of_mem _ (mem_uIcc_of_le hc.2.le hd.1.le)
  have h2g : IntervalIntegrable g volume (f a) (f x) := by
    refine' hg1.mono_set _
    rw [← hf.image_uIcc]
    exact hf.surjOn_uIcc left_mem_uIcc (Ioo_subset_Icc_self hx)
  have h3g : StronglyMeasurableAtFilter g (𝓝[J] f x) :=
    hg_cont.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc (f x)
  haveI : Fact (f x ∈ J) := ⟨h2x⟩
  have : HasDerivWithinAt (fun u => ∫ x in f a..u, g x) (g (f x)) J (f x) :=
    intervalIntegral.integral_hasDerivWithinAt_right h2g h3g (hg_cont (f x) h2x)
  refine' (this.scomp x ((hff' x hx).Ioo_of_Ioi hd.1) _).Ioi_of_Ioo hd.1
  rw [← hJ]
  refine' (mapsTo_image _ _).mono _ Subset.rfl
  exact Ioo_subset_Icc_self.trans ((Icc_subset_Icc_left hc.2.le).trans Icc_subset_uIcc)
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntervalIntegrable (fun x => f' x • (g ∘ f) x) volume a b
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
h_der :
  ∀ (x : ℝ),
    x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
⊢ (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) = ∫ (u : ℝ) in f a..f b, g u
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
h_der :
  ∀ (x : ℝ),
    x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
⊢ (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) = ∫ (u : ℝ) in f a..f b, g u
rw [← intervalIntegrable_iff'] at hg2
no goals
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntervalIntegrable (fun x => f' x • (g ∘ f) x) volume a b
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
h_der :
  ∀ (x : ℝ),
    x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
⊢ (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) = ∫ (u : ℝ) in f a..f b, g u
simp_rw [integral_eq_sub_of_hasDeriv_right h_cont h_der hg2, integral_same, sub_zero]
case refine'_1
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ f a ∈ [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]

case refine'_2
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ MapsTo (fun u => f u) [[a, b]] [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
refine' (continuousOn_primitive_interval' hg1 _).comp hf _
case refine'_1
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ f a ∈ f '' [[a, b]]
case refine'_1
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ f a ∈ [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
rw [← hf.image_uIcc]
no goals
case refine'_1
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ f a ∈ f '' [[a, b]]
exact mem_image_of_mem f left_mem_uIcc
case refine'_2
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ MapsTo (fun u => f u) [[a, b]] (f '' [[a, b]])
case refine'_2
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ MapsTo (fun u => f u) [[a, b]] [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
rw [← hf.image_uIcc]
no goals
case refine'_2
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ MapsTo (fun u => f u) [[a, b]] (f '' [[a, b]])
exact mapsTo_image _ _
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
⊢ ∀ (x : ℝ),
    x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
intro x hx
case intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
obtain ⟨c, hc⟩ := nonempty_Ioo.mpr hx.1
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
case intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
obtain ⟨d, hd⟩ := nonempty_Ioo.mpr hx.2
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
have cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b) := by
  rw [uIcc_of_le (hc.2.trans hd.1).le]
  exact Icc_subset_Ioo hc.1 hd.2
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
hg_cont : ContinuousOn g (f '' [[c, d]])
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
replace hg_cont := hg_cont.mono (image_subset f cdsub)
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
hg_cont : ContinuousOn g (f '' [[c, d]])
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
hg_cont : ContinuousOn g (f '' [[c, d]])
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
let J := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
hg_cont : ContinuousOn g (f '' [[c, d]])
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hJ : f '' [[c, d]] = J
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
hg_cont : ContinuousOn g (f '' [[c, d]])
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
have hJ : f '' [[c, d]] = J := (hf.mono (cdsub.trans Ioo_subset_Icc_self)).image_uIcc
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
hg_cont : ContinuousOn g (f '' [[c, d]])
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hJ : f '' [[c, d]] = J
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
rw [hJ] at hg_cont
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
have h2x : f x ∈ J := by rw [← hJ]; exact mem_image_of_mem _ (mem_uIcc_of_le hc.2.le hd.1.le)
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
have h2g : IntervalIntegrable g volume (f a) (f x) := by
  refine' hg1.mono_set _
  rw [← hf.image_uIcc]
  exact hf.surjOn_uIcc left_mem_uIcc (Ioo_subset_Icc_self hx)
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
have h3g : StronglyMeasurableAtFilter g (𝓝[J] f x) :=
  hg_cont.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc (f x)
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x)
this : Fact (f x ∈ J)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
haveI : Fact (f x ∈ J) := ⟨h2x⟩
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x)
this✝ : Fact (f x ∈ J)
this : HasDerivWithinAt (fun u => ∫ (x : ℝ) in f a..u, g x) (g (f x)) J (f x)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x)
this : Fact (f x ∈ J)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
have : HasDerivWithinAt (fun u => ∫ x in f a..u, g x) (g (f x)) J (f x) :=
  intervalIntegral.integral_hasDerivWithinAt_right h2g h3g (hg_cont (f x) h2x)
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x)
this✝ : Fact (f x ∈ J)
this : HasDerivWithinAt (fun u => ∫ (x : ℝ) in f a..u, g x) (g (f x)) J (f x)
⊢ MapsTo f (Ioo x d) J
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x)
this✝ : Fact (f x ∈ J)
this : HasDerivWithinAt (fun u => ∫ (x : ℝ) in f a..u, g x) (g (f x)) J (f x)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
refine' (this.scomp x ((hff' x hx).Ioo_of_Ioi hd.1) _).Ioi_of_Ioo hd.1
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x)
this✝ : Fact (f x ∈ J)
this : HasDerivWithinAt (fun u => ∫ (x : ℝ) in f a..u, g x) (g (f x)) J (f x)
⊢ MapsTo f (Ioo x d) (f '' [[c, d]])
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x)
this✝ : Fact (f x ∈ J)
this : HasDerivWithinAt (fun u => ∫ (x : ℝ) in f a..u, g x) (g (f x)) J (f x)
⊢ MapsTo f (Ioo x d) J
rw [← hJ]
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x)
this✝ : Fact (f x ∈ J)
this : HasDerivWithinAt (fun u => ∫ (x : ℝ) in f a..u, g x) (g (f x)) J (f x)
⊢ Ioo x d ⊆ [[c, d]]
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x)
this✝ : Fact (f x ∈ J)
this : HasDerivWithinAt (fun u => ∫ (x : ℝ) in f a..u, g x) (g (f x)) J (f x)
⊢ MapsTo f (Ioo x d) (f '' [[c, d]])
refine' (mapsTo_image _ _).mono _ Subset.rfl
no goals
case intro.intro
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x)
this✝ : Fact (f x ∈ J)
this : HasDerivWithinAt (fun u => ∫ (x : ℝ) in f a..u, g x) (g (f x)) J (f x)
⊢ Ioo x d ⊆ [[c, d]]
exact Ioo_subset_Icc_self.trans ((Icc_subset_Icc_left hc.2.le).trans Icc_subset_uIcc)
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
⊢ Icc c d ⊆ Ioo (min a b) (max a b)
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
⊢ [[c, d]] ⊆ Ioo (min a b) (max a b)
rw [uIcc_of_le (hc.2.trans hd.1).le]
no goals
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
⊢ Icc c d ⊆ Ioo (min a b) (max a b)
exact Icc_subset_Ioo hc.1 hd.2
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
⊢ f x ∈ f '' [[c, d]]
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
⊢ f x ∈ J
rw [← hJ]
no goals
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
⊢ f x ∈ f '' [[c, d]]
exact mem_image_of_mem _ (mem_uIcc_of_le hc.2.le hd.1.le)
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
⊢ [[f a, f x]] ⊆ [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
⊢ IntervalIntegrable g volume (f a) (f x)
refine' hg1.mono_set _
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
⊢ [[f a, f x]] ⊆ f '' [[a, b]]
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
⊢ [[f a, f x]] ⊆ [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
rw [← hf.image_uIcc]
no goals
ι : Type ?u.1890572
𝕜 : Type ?u.1890575
E : Type u_1
F : Type ?u.1890581
A : Type ?u.1890584
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
⊢ [[f a, f x]] ⊆ f '' [[a, b]]
exact hf.surjOn_uIcc left_mem_uIcc (Ioo_subset_Icc_self hx)