-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem norm_image_sub_le_of_norm_hasFDerivWithin_le
    (hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (bound : ∀ x ∈ s, ‖f' x‖ ≤ C) (hs : Convex ℝ s)
    (xs : x ∈ s) (ys : y ∈ s) : ‖f y - f x‖ ≤ C * ‖y - x‖

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
g : ℝ → E := ⇑(AffineMap.lineMap x y)
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Tactic:
have segm : MapsTo g (Icc 0 1 : Set ℝ) s := hs.mapsTo_lineMap xs ys

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
g : ℝ → E := ⇑(AffineMap.lineMap x y)
segm : MapsTo g (Icc 0 1) s
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound✝ : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
g : ℝ → E := ⇑(AffineMap.lineMap x y)
segm : MapsTo g (Icc 0 1) s
hD : ∀ t ∈ Icc 0 1, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) (Icc 0 1) t
bound : ∀ t ∈ Ico 0 1, ‖(f' (g t)) (y - x)‖ ≤ C * ‖y - x‖
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Tactic:
simpa [g] using norm_image_sub_le_of_norm_deriv_le_segment_01' hD bound

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Tactic:
set g := (AffineMap.lineMap x y : ℝ → E)

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
g : ℝ → E := ⇑(AffineMap.lineMap x y)
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
g : ℝ → E := ⇑(AffineMap.lineMap x y)
segm : MapsTo g (Icc 0 1) s
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Tactic:
have hD : ∀ t ∈ Icc (0 : ℝ) 1,
    HasDerivWithinAt (f ∘ g) (f' (g t) (y - x)) (Icc 0 1) t := fun t ht => by
  simpa using ((hf (g t) (segm ht)).restrictScalars ℝ).comp_hasDerivWithinAt _
    AffineMap.hasDerivWithinAt_lineMap segm

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
g : ℝ → E := ⇑(AffineMap.lineMap x y)
segm : MapsTo g (Icc 0 1) s
hD : ∀ t ∈ Icc 0 1, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) (Icc 0 1) t
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
g : ℝ → E := ⇑(AffineMap.lineMap x y)
segm : MapsTo g (Icc 0 1) s
hD : ∀ t ∈ Icc 0 1, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) (Icc 0 1) t
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Tactic:
have bound : ∀ t ∈ Ico (0 : ℝ) 1, ‖f' (g t) (y - x)‖ ≤ C * ‖y - x‖ := fun t ht =>
  le_of_opNorm_le _ (bound _ <| segm <| Ico_subset_Icc_self ht) _

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound✝ : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
g : ℝ → E := ⇑(AffineMap.lineMap x y)
segm : MapsTo g (Icc 0 1) s
hD : ∀ t ∈ Icc 0 1, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) (Icc 0 1) t
bound : ∀ t ∈ Ico 0 1, ‖(f' (g t)) (y - x)‖ ≤ C * ‖y - x‖
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Tactic:
letI : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖