awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
K : ℝ≥0
hK : ‖f'‖₊ < K
⊢ IsBigOWith.{u_2, u_3, u_2} (E := F) (F := E) (↑K : ℝ) (𝓝 (x, x))
    (fun (x : E × E) ↦
      HAdd.hAdd (β := F) (HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F))
        ((f' : (a : E) → F) (x.1 - x.2) : F))
    fun (p : E × E) ↦ p.1 - p.2

Tactic:
have := hf.isLittleO.add_isBigOWith (f'.isBigOWith_comp _ _) hK
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
K : ℝ≥0
hK : ‖f'‖₊ < K
this :
  IsBigOWith.{u_2, u_3, u_2} (E := F) (F := E) (↑K : ℝ) (𝓝 (x, x))
    (fun (x : E × E) ↦
      HAdd.hAdd (β := F) (HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F))
        ((f' : (a : E) → F) (x.1 - x.2) : F))
    fun (p : E × E) ↦ p.1 - p.2
⊢ ∀ᶠ (x : E × E) in 𝓝 (x, x), ‖f x.1 - f x.2‖ ≤ (↑K : ℝ) * ‖x.1 - x.2‖

Tactic:
simp only [sub_add_cancel, IsBigOWith] at this

Premises used: Asymptotics.IsBigOWith, sub_add_cancel
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : 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‖
rcases :
  ∀ (U : Set E) (Uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (xU : x ∈ U)
    (hU : U ×ˢ U ⊆ {x : E × E | (fun (x : E × E) ↦ ‖f x.1 - f x.2‖ ≤ (↑K : ℝ) * ‖x.1 - x.2‖) x}),
    ∃ s ∈ 𝓝 x, LipschitzOnWith K f s
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s

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

Premises used: exists_nhds_square
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : 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[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
xU : x ∈ U
hU : U ×ˢ U ⊆ {x : E × E | (fun (x : E × E) ↦ ‖f x.1 - f x.2‖ ≤ (↑K : ℝ) * ‖x.1 - x.2‖) x}
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s

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

Premises used: Iff.mpr, And.intro, IsOpen.mem_nhds, Exists.intro, Set.mk_mem_prod, lipschitzOnWith_iff_norm_sub_le
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : 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[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
xU : x ∈ U
hU : U ×ˢ U ⊆ {x : E × E | (fun (x : E × E) ↦ ‖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)⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
⊢ ∃ (K : ℝ≥0), ∃ s ∈ 𝓝 x, LipschitzOnWith K f s

Tactic:
(exists_gt _).imp hf.exists_lipschitzOnWith_of_nnnorm_lt

Premises used: NoMaxOrder.exists_gt, Exists.imp, HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ‖f'‖ ≤ C

Tactic:
le_of_forall_pos_le_add fun ε ε0 => opNorm_le_of_nhds_zero ?_ ?_

Premises used: le_of_forall_pos_le_add, ContinuousLinearMap.opNorm_le_of_nhds_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
refine_1 : ∀ (ε : ℝ) (ε0 : 0 < ε), 0 ≤ C + ε
refine_2 : ∀ (ε : ℝ) (ε0 : 0 < ε), ∀ᶠ (x : E) in 𝓝 0, norm.{u_3} (E := F) ((f' : (a : E) → F) x : F) ≤ (C + ε) * ‖x‖
⊢ ‖f'‖ ≤ C

Tactic:
refine le_of_forall_pos_le_add fun ε ε0 => opNorm_le_of_nhds_zero ?_ ?_

Premises used: le_of_forall_pos_le_add, ContinuousLinearMap.opNorm_le_of_nhds_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
ε : ℝ
ε0 : 0 < ε
⊢ 0 ≤ C + ε

Tactic:
add_nonneg hC₀ ε0.le

Premises used: LT.lt.le, add_nonneg
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
ε : ℝ
ε0 : 0 < ε
⊢ 0 ≤ C + ε

Tactic:
exact add_nonneg hC₀ ε0.le

Premises used: LT.lt.le, add_nonneg
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
ε : ℝ
ε0 : 0 < ε
refine_2 :
  ∀ (hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖) (ε : ℝ) (ε0 : 0 < ε),
    ∀ᶠ (x : E) in 𝓝 0, norm.{u_3} (E := F) ((f' : (a : E) → F) x : F) ≤ (C + ε) * ‖x‖
⊢ ∀ᶠ (x : E) in 𝓝 0, norm.{u_3} (E := F) ((f' : (a : E) → F) x : F) ≤ (C + ε) * ‖x‖

Tactic:
rw [← map_add_left_nhds_zero x₀, eventually_map] at hlip

Premises used: Filter.eventually_map, map_add_left_nhds_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖
ε : ℝ
ε0 : 0 < ε
h :
  ∀ (y : E) (hy : ‖HSub.hSub (β := F) (f (x₀ + y) - f x₀) ((f' : (a : E) → F) y : F)‖ ≤ ε * ‖y‖)
    (hyC : ‖f (x₀ + y) - f x₀‖ ≤ C * ‖x₀ + y - x₀‖), norm.{u_3} (E := F) ((f' : (a : E) → F) y : F) ≤ (C + ε) * ‖y‖
⊢ ∀ᶠ (x : E) in 𝓝 0, norm.{u_3} (E := F) ((f' : (a : E) → F) x : F) ≤ (C + ε) * ‖x‖

Tactic:
filter_upwards [isLittleO_iff.1 (hasFDerivAt_iff_isLittleO_nhds_zero.1 hf) ε0, hlip] with y hy hyC

Premises used: Iff.mp, Asymptotics.isLittleO_iff, hasFDerivAt_iff_isLittleO_nhds_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖
ε : ℝ
ε0 : 0 < ε
y : E
hy : ‖HSub.hSub (β := F) (f (x₀ + y) - f x₀) ((f' : (a : E) → F) y : F)‖ ≤ ε * ‖y‖
hyC : ‖f (x₀ + y) - f x₀‖ ≤ C * ‖x₀ + y - x₀‖
⊢ ‖f (x₀ + y) - f x₀‖ ≤ C * ‖y‖

Tactic:
rw [add_sub_cancel_left] at hyC

Premises used: add_sub_cancel_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖
ε : ℝ
ε0 : 0 < ε
y : E
hy : ‖HSub.hSub (β := F) (f (x₀ + y) - f x₀) ((f' : (a : E) → F) y : F)‖ ≤ ε * ‖y‖
hyC : ‖f (x₀ + y) - f x₀‖ ≤ C * ‖y‖
⊢ norm.{u_3} (E := F) ((f' : (a : E) → F) y : F) ≤
    ‖f (x₀ + y) - f x₀‖ + ‖HSub.hSub (β := F) (f (x₀ + y) - f x₀) ((f' : (a : E) → F) y : F)‖

Tactic:
norm_le_insert _ _

Premises used: norm_le_insert
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖
ε : ℝ
ε0 : 0 < ε
y : E
hy : ‖HSub.hSub (β := F) (f (x₀ + y) - f x₀) ((f' : (a : E) → F) y : F)‖ ≤ ε * ‖y‖
hyC : ‖f (x₀ + y) - f x₀‖ ≤ C * ‖y‖
⊢ ‖f (x₀ + y) - f x₀‖ + ‖HSub.hSub (β := F) (f (x₀ + y) - f x₀) ((f' : (a : E) → F) y : F)‖ ≤ C * ‖y‖ + ε * ‖y‖

Tactic:
add_le_add hyC hy

Premises used: add_le_add
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖
ε : ℝ
ε0 : 0 < ε
y : E
hy : ‖HSub.hSub (β := F) (f (x₀ + y) - f x₀) ((f' : (a : E) → F) y : F)‖ ≤ ε * ‖y‖
hyC : ‖f (x₀ + y) - f x₀‖ ≤ C * ‖y‖
⊢ C * ‖y‖ + ε * ‖y‖ = (C + ε) * ‖y‖

Tactic:
(add_mul _ _ _).symm

Premises used: add_mul, Eq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖
ε : ℝ
ε0 : 0 < ε
y : E
hy : ‖HSub.hSub (β := F) (f (x₀ + y) - f x₀) ((f' : (a : E) → F) y : F)‖ ≤ ε * ‖y‖
hyC : ‖f (x₀ + y) - f x₀‖ ≤ C * ‖y‖
⊢ norm.{u_3} (E := F) ((f' : (a : E) → F) y : F) ≤ (C + ε) * ‖y‖

Tactic:
calc
    ‖f' y‖ ≤ ‖f (x₀ + y) - f x₀‖ + ‖f (x₀ + y) - f x₀ - f' y‖ := norm_le_insert _ _
    _ ≤ C * ‖y‖ + ε * ‖y‖ := add_le_add hyC hy
    _ = (C + ε) * ‖y‖ := (add_mul _ _ _).symm

Premises used: add_mul, add_le_add, HAdd.hAdd, norm_le_insert, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖f'‖ ≤ (↑C : ℝ)

Tactic:
hf.le_of_lip' C.coe_nonneg ?_

Premises used: HasFDerivAt.le_of_lip', NNReal.coe_nonneg
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
refine : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
⊢ ‖f'‖ ≤ (↑C : ℝ)

Tactic:
refine hf.le_of_lip' C.coe_nonneg ?_

Premises used: HasFDerivAt.le_of_lip', NNReal.coe_nonneg
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
x : E
hx : x ∈ s
⊢ ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖

Tactic:
hlip.norm_sub_le hx (mem_of_mem_nhds hs)

Premises used: LipschitzOnWith.norm_sub_le, mem_of_mem_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E | x ∈ s → Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖) x} x} a
h₁ h₂ : ∀ (x : E) (hx : x ∈ s), ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖

Tactic:
filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ≥0
hlip : LipschitzWith C f
⊢ ‖f'‖ ≤ (↑C : ℝ)

Tactic:
hf.le_of_lipschitzOn univ_mem (lipschitzOnWith_univ.2 hlip)

Premises used: Iff.mpr, HasFDerivAt.le_of_lipschitzOn, lipschitzOnWith_univ, Filter.univ_mem
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
pos : ∀ (hf : DifferentiableAt 𝕜 f x₀), norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ C
neg : ∀ (hf : ¬DifferentiableAt 𝕜 f x₀), norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ C
⊢ norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ C

Tactic:
by_cases hf : DifferentiableAt 𝕜 f x₀

Premises used: DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
hf : DifferentiableAt 𝕜 f x₀
⊢ norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ C

Tactic:
hf.hasFDerivAt.le_of_lip' hC₀ hlip

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.le_of_lip'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
hf : DifferentiableAt 𝕜 f x₀
⊢ norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ C

Tactic:
exact hf.hasFDerivAt.le_of_lip' hC₀ hlip

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.le_of_lip'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
hf : ¬DifferentiableAt 𝕜 f x₀
neg : norm (E := E →L[𝕜] F) 0 ≤ C
⊢ norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ C

Tactic:
rw [fderiv_zero_of_not_differentiableAt hf]

Premises used: fderiv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
hf : ¬DifferentiableAt 𝕜 f x₀
⊢ norm (E := E →L[𝕜] F) 0 ≤ C

Tactic:
simp [hC₀]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ (↑C : ℝ)

Tactic:
norm_fderiv_le_of_lip' 𝕜 C.coe_nonneg ?_

Premises used: NNReal.coe_nonneg, norm_fderiv_le_of_lip'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
refine : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
⊢ norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ (↑C : ℝ)

Tactic:
refine norm_fderiv_le_of_lip' 𝕜 C.coe_nonneg ?_

Premises used: NNReal.coe_nonneg, norm_fderiv_le_of_lip'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
x : E
hx : x ∈ s
⊢ ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖

Tactic:
hlip.norm_sub_le hx (mem_of_mem_nhds hs)

Premises used: LipschitzOnWith.norm_sub_le, mem_of_mem_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E | x ∈ s → Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖) x} x} a
h₁ h₂ : ∀ (x : E) (hx : x ∈ s), ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖

Tactic:
filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ≥0
hlip : LipschitzWith C f
⊢ norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ (↑C : ℝ)

Tactic:
norm_fderiv_le_of_lipschitzOn 𝕜 univ_mem (lipschitzOnWith_univ.2 hlip)

Premises used: Iff.mpr, lipschitzOnWith_univ, norm_fderiv_le_of_lipschitzOn, Filter.univ_mem
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
V : Type u_2
V' : Type u_3
W : Type u_4
W' : Type u_5
inst : NontriviallyNormedField 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : NormedAddCommGroup V'
inst_4 : NormedSpace 𝕜 V'
inst_5 : NormedAddCommGroup W
inst_6 : NormedSpace 𝕜 W
inst_7 : NormedAddCommGroup W'
inst_8 : NormedSpace 𝕜 W'
inst_9 : RingHomIsometric σ
inst_10 : RingHomInvPair σ σ'
L : W →SL[σ] W'
R : V' →SL[σ'] V
f : V → W
z : V'
f' : V →L[𝕜] W
hf : HasFDerivAt f f' ((R : (a : V') → V) z)
⊢ RingHomIsometric σ'

Tactic:
have : RingHomIsometric σ' := .inv σ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
V : Type u_2
V' : Type u_3
W : Type u_4
W' : Type u_5
inst : NontriviallyNormedField 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : NormedAddCommGroup V'
inst_4 : NormedSpace 𝕜 V'
inst_5 : NormedAddCommGroup W
inst_6 : NormedSpace 𝕜 W
inst_7 : NormedAddCommGroup W'
inst_8 : NormedSpace 𝕜 W'
inst_9 : RingHomIsometric σ
inst_10 : RingHomInvPair σ σ'
L : W →SL[σ] W'
R : V' →SL[σ'] V
f : V → W
z : V'
f' : V →L[𝕜] W
hf : HasFDerivAt f f' ((R : (a : V') → V) z)
this : RingHomIsometric σ'
rw :
  ∀
    (hf :
      IsLittleO.{u_2, u_4, u_2} (E := W) (F := V) (𝓝 0)
        (fun (h : V) ↦
          HSub.hSub (β := W) (f (HAdd.hAdd (α := V) ((R : (a : V') → V) z : V) h) - f ((R : (a : V') → V) z))
            ((f' : (a : V) → W) h : W))
        fun (h : V) ↦ h)
    (this : RingHomIsometric σ'),
    IsLittleO.{u_3, u_5, u_3} (E := W') (F := V') (𝓝 0)
      (fun (h : V') ↦
        HSub.hSub (β := W')
          (HSub.hSub (α := W') (((⇑L : (a : W) → W') ∘ f ∘ (⇑R : (a : V') → V)) (z + h))
            (((⇑L : (a : W) → W') ∘ f ∘ (⇑R : (a : V') → V)) z))
          ((L ∘SL f' ∘SL R : (a : V') → W') h : W'))
      fun (h : V') ↦ h
⊢ HasFDerivAt ((⇑L : (a : W) → W') ∘ f ∘ (⇑R : (a : V') → V)) (L ∘SL f' ∘SL R) z

Tactic:
rw [hasFDerivAt_iff_isLittleO_nhds_zero] at ⊢ hf

Premises used: hasFDerivAt_iff_isLittleO_nhds_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
V : Type u_2
V' : Type u_3
W : Type u_4
W' : Type u_5
inst : NontriviallyNormedField 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : NormedAddCommGroup V'
inst_4 : NormedSpace 𝕜 V'
inst_5 : NormedAddCommGroup W
inst_6 : NormedSpace 𝕜 W
inst_7 : NormedAddCommGroup W'
inst_8 : NormedSpace 𝕜 W'
inst_9 : RingHomIsometric σ
inst_10 : RingHomInvPair σ σ'
L : W →SL[σ] W'
R : V' →SL[σ'] V
f : V → W
z : V'
f' : V →L[𝕜] W
hf :
  IsLittleO.{u_2, u_4, u_2} (E := W) (F := V) (𝓝 0)
    (fun (h : V) ↦
      HSub.hSub (β := W) (f (HAdd.hAdd (α := V) ((R : (a : V') → V) z : V) h) - f ((R : (a : V') → V) z))
        ((f' : (a : V) → W) h : W))
    fun (h : V) ↦ h
this : RingHomIsometric σ'
⊢ IsLittleO.{u_3, u_4, u_2} (α := V') (E := W) (F := V) (𝓝 0)
    ((fun (h : V) ↦
        HSub.hSub (β := W) (f (HAdd.hAdd (α := V) ((R : (a : V') → V) z : V) h) - f ((R : (a : V') → V) z))
          ((f' : (a : V) → W) h : W)) ∘
      (⇑R : (a : V') → V))
    ((fun (h : V) ↦ h) ∘ (⇑R : (a : V') → V))

Tactic:
have := hf.comp_tendsto (R.map_zero ▸ R.continuous.continuousAt.tendsto)