-- Mathlib/Analysis/Calculus/ContDiff/RCLike.lean
theorem ContDiffWithinAt.exists_lipschitzOnWith {E F : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E}
    (hf : ContDiffWithinAt ℝ 1 f s x) (hs : Convex ℝ s) :
    ∃ K : ℝ≥0, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Proof state:
case intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
t : Set E
hst : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries ℝ E F
hp : HasFTaylorSeriesUpToOn (↑1) f p t
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
rcases Metric.mem_nhdsWithin_iff.mp hst with ⟨ε, ε0, hε⟩

Result:
case intro.intro.intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
t : Set E
hst : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries ℝ E F
hp : HasFTaylorSeriesUpToOn (↑1) f p t
ε : ℝ
ε0 : ε > 0
hε : Metric.ball x ε ∩ insert x s ⊆ t
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
rcases hf 1 le_rfl with ⟨t, hst, p, hp⟩

Result:
case intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
t : Set E
hst : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries ℝ E F
hp : HasFTaylorSeriesUpToOn (↑1) f p t
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Proof state:
case intro.intro.intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
t : Set E
hst : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries ℝ E F
hp : HasFTaylorSeriesUpToOn (↑1) f p t
ε : ℝ
ε0 : ε > 0
hε : Metric.ball x ε ∩ insert x s ⊆ t
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
replace hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s) := hp.mono hε

Result:
case intro.intro.intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
t : Set E
hst : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hε : Metric.ball x ε ∩ insert x s ⊆ t
hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s)
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
K : ℝ≥0
t : Set E
hst : t ∈ 𝓝[Metric.ball x ε ∩ s] x
hft : LipschitzOnWith K f t
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
rw [inter_comm, ← nhdsWithin_restrict' _ (Metric.ball_mem_nhds _ ε0)] at hst

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
K : ℝ≥0
t : Set E
hst : t ∈ 𝓝[s] x
hft : LipschitzOnWith K f t
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Proof state:
case intro.intro.intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
rcases hp.exists_lipschitzOnWith ((convex_ball _ _).inter hs) with ⟨K, t, hst, hft⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
K : ℝ≥0
t : Set E
hst : t ∈ 𝓝[Metric.ball x ε ∩ s] x
hft : LipschitzOnWith K f t
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Proof state:
case intro.intro.intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s)
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
rw [← insert_eq_of_mem (Metric.mem_ball_self ε0), ← insert_inter_distrib] at hp

Result:
case intro.intro.intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Proof state:
case intro.intro.intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
t : Set E
hst : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hε : Metric.ball x ε ∩ insert x s ⊆ t
hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s)
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
clear hst hε t

Result:
case intro.intro.intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s)
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
K : ℝ≥0
t : Set E
hst : t ∈ 𝓝[s] x
hft : LipschitzOnWith K f t
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
exact ⟨K, t, hst, hft⟩

Result:
no goals