E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
set g : ℝ → E := fun t => AffineMap.lineMap x y t
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
set I := Icc (0 : ℝ) 1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
have hsub : Ioo (0 : ℝ) 1 ⊆ I := Ioo_subset_Icc_self
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
have hmaps : MapsTo g I s := hs.mapsTo_lineMap xs ys
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
have hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) (f' (g t) (y - x)) I t := fun t ht =>
  (hf _ (hmaps ht)).comp_hasDerivWithinAt t AffineMap.hasDerivWithinAt_lineMap hmaps
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
t : ℝ
Ht : t ∈ Ioo 0 1
hMVT' : ↑(f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
hMVT : ∃ t, t ∈ Ioo 0 1 ∧ ↑(f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
rcases hMVT with ⟨t, Ht, hMVT'⟩
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
t : ℝ
Ht : t ∈ Ioo 0 1
hMVT' : ↑(f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)
⊢ ∃ x_1, x_1 ∈ Icc 0 1 ∧ f y - f x = ↑(f' (↑(AffineMap.lineMap x y) x_1)) (y - x)
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
t : ℝ
Ht : t ∈ Ioo 0 1
hMVT' : ↑(f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)
⊢ ∃ z, z ∈ segment ℝ x y ∧ f y - f x = ↑(f' z) (y - x)
rw [segment_eq_image_lineMap, bex_image_iff]
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
t : ℝ
Ht : t ∈ Ioo 0 1
hMVT' : ↑(f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)
⊢ f y - f x = ↑(f' (↑(AffineMap.lineMap x y) t)) (y - x)
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
t : ℝ
Ht : t ∈ Ioo 0 1
hMVT' : ↑(f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)
⊢ ∃ x_1, x_1 ∈ Icc 0 1 ∧ f y - f x = ↑(f' (↑(AffineMap.lineMap x y) x_1)) (y - x)
refine ⟨t, hsub Ht, ?_⟩
no goals
case intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
t : ℝ
Ht : t ∈ Ioo 0 1
hMVT' : ↑(f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)
⊢ f y - f x = ↑(f' (↑(AffineMap.lineMap x y) t)) (y - x)
simpa using hMVT'.symm
case refine'_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
⊢ ContinuousOn (f ∘ g) (Icc 0 1)

case refine'_2
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
⊢ ∀ (x_1 : ℝ), x_1 ∈ Ioo 0 1 → HasDerivAt (f ∘ g) (↑(f' (g x_1)) (y - x)) x_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
⊢ ∃ t, t ∈ Ioo 0 1 ∧ ↑(f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)
refine' exists_hasDerivAt_eq_slope (f ∘ g) _ (by norm_num) _ _
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
⊢ 0 < 1
norm_num
no goals
case refine'_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
⊢ ContinuousOn (f ∘ g) (Icc 0 1)
exact fun t Ht => (hfg t Ht).continuousWithinAt
no goals
case refine'_2
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.474056
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → ℝ
s : Set E
x y : E
f' : E → E →L[ℝ] ℝ
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t => ↑(AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ (t : ℝ), t ∈ I → HasDerivWithinAt (f ∘ g) (↑(f' (g t)) (y - x)) I t
⊢ ∀ (x_1 : ℝ), x_1 ∈ Ioo 0 1 → HasDerivAt (f ∘ g) (↑(f' (g x_1)) (y - x)) x_1
exact fun t Ht => (hfg t <| hsub Ht).hasDerivAt (Icc_mem_nhds Ht.1 Ht.2)