-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt (hf : HasStrictFDerivAt f f' x)
    (K : ℝ≥0) (hK : ‖f'‖₊ < K) : ∃ s ∈ 𝓝 x, LipschitzOnWith K f s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
K : ℝ≥0
hK : ‖f'‖₊ < K
this :
  IsBigOWith ((fun a => ↑a) K) (𝓝 (x, x)) (fun x => f x.1 - f x.2 - f' (x.1 - x.2) + f' (x.1 - x.2)) fun p => p.1 - p.2
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s

Tactic:
simp only [sub_add_cancel, IsBigOWith] at this

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
K : ℝ≥0
hK : ‖f'‖₊ < K
this : ∀ᶠ (x : E × E) in 𝓝 (x, x), ‖f x.1 - f x.2‖ ≤ ↑K * ‖x.1 - x.2‖
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
K : ℝ≥0
hK : ‖f'‖₊ < K
this : ∀ᶠ (x : E × E) in 𝓝 (x, x), ‖f x.1 - f x.2‖ ≤ ↑K * ‖x.1 - x.2‖
U : Set E
Uo : IsOpen U
xU : x ∈ U
hU : U ×ˢ U ⊆ {x | (fun x => ‖f x.1 - f x.2‖ ≤ ↑K * ‖x.1 - x.2‖) x}
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s

Tactic:
exact
  ⟨U, Uo.mem_nhds xU, lipschitzOnWith_iff_norm_sub_le.2 fun x hx y hy => hU (mk_mem_prod hx hy)⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
K : ℝ≥0
hK : ‖f'‖₊ < K
this : ∀ᶠ (x : E × E) in 𝓝 (x, x), ‖f x.1 - f x.2‖ ≤ ↑K * ‖x.1 - x.2‖
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s

Tactic:
rcases exists_nhds_square this with ⟨U, Uo, xU, hU⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
K : ℝ≥0
hK : ‖f'‖₊ < K
this : ∀ᶠ (x : E × E) in 𝓝 (x, x), ‖f x.1 - f x.2‖ ≤ ↑K * ‖x.1 - x.2‖
U : Set E
Uo : IsOpen U
xU : x ∈ U
hU : U ×ˢ U ⊆ {x | (fun x => ‖f x.1 - f x.2‖ ≤ ↑K * ‖x.1 - x.2‖) x}
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
K : ℝ≥0
hK : ‖f'‖₊ < K
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s

Tactic:
have := hf.isLittleO.add_isBigOWith (f'.isBigOWith_comp _ _) hK

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
K : ℝ≥0
hK : ‖f'‖₊ < K
this :
  IsBigOWith ((fun a => ↑a) K) (𝓝 (x, x)) (fun x => f x.1 - f x.2 - f' (x.1 - x.2) + f' (x.1 - x.2)) fun p => p.1 - p.2
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s