awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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
rw :
  HasFDerivWithinAt f f' univ x ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝 x) (𝓝 0)
rw₁ :
  Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝[univ] x) (𝓝 0) ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝 x) (𝓝 0)
⊢ HasFDerivAt f f' x ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝 x) (𝓝 0)
have rw₂ : Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖) (𝓝 x)
    (𝓝 0) ↔
  Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
    (𝓝 x) (𝓝 0)
Tactic: rw [← hasFDerivWithinAt_univ, hasFDerivWithinAt_iff_tendsto, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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
⊢ HasFDerivAt f f' x ↔
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝 0)
      (fun (h : E) ↦ HSub.hSub (β := F) (f (x + h) - f x) ((f' : (a : E) → F) h : F)) fun (h : E) ↦ h
have rw : IsLittleO.{u_2, u_3, u_2} (α := E) (E := F) (F := E) (𝓝 0)
    ((fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) ∘ fun (x_1 : E) ↦ x + x_1)
    ((fun (x' : E) ↦ x' - x) ∘ fun (x_1 : E) ↦ x + x_1) ↔
  IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝 0)
    (fun (h : E) ↦ HSub.hSub (β := F) (f (x + h) - f x) ((f' : (a : E) → F) h : F)) fun (h : E) ↦ h
Tactic: rw [hasFDerivAt_iff_isLittleO, ← map_add_left_nhds_zero x, isLittleO_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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
n : ℕ
h : IsBigO (F := ℝ) (𝓝[s] x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : 1 < n
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x₀
have simp_rw : IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀)
  (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x₀) ((0 : (a : E) → F) (x' - x₀) : F)) fun (x' : E) ↦ x' - x₀
Tactic: simp_rw [hasFDerivWithinAt_iff_isLittleO,
    h.eq_zero_of_norm_pow_within hx₀ hn.ne_bot, zero_apply, sub_zero,
    h.trans_isLittleO ((isLittleO_pow_sub_sub x₀ hn).mono nhdsWithin_le_nhds)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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
n : ℕ
h : IsBigO (F := ℝ) (𝓝[s] x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : 1 < n
simp_rw :
  IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x₀) ((0 : (a : E) → F) (x' - x₀) : F)) fun (x' : E) ↦ x' - x₀
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x₀
have simp_rw₁ : IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀)
  (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - 0) ((0 : (a : E) → F) (x' - x₀) : F)) fun (x' : E) ↦ x' - x₀
Tactic: simp_rw [hasFDerivWithinAt_iff_isLittleO,
    h.eq_zero_of_norm_pow_within hx₀ hn.ne_bot, zero_apply, sub_zero,
    h.trans_isLittleO ((isLittleO_pow_sub_sub x₀ hn).mono nhdsWithin_le_nhds)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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
n : ℕ
h : IsBigO (F := ℝ) (𝓝[s] x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : 1 < n
simp_rw :
  IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x₀) ((0 : (a : E) → F) (x' - x₀) : F)) fun (x' : E) ↦ x' - x₀
simp_rw₁ :
  IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - 0) ((0 : (a : E) → F) (x' - x₀) : F)) fun (x' : E) ↦ x' - x₀
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x₀
have simp_rw₂ : IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀) (fun (x' : E) ↦ f x' - 0 - 0) fun (x' : E) ↦ x' - x₀
Tactic: simp_rw [hasFDerivWithinAt_iff_isLittleO,
    h.eq_zero_of_norm_pow_within hx₀ hn.ne_bot, zero_apply, sub_zero,
    h.trans_isLittleO ((isLittleO_pow_sub_sub x₀ hn).mono nhdsWithin_le_nhds)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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
n : ℕ
h : IsBigO (F := ℝ) (𝓝[s] x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : 1 < n
simp_rw :
  IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x₀) ((0 : (a : E) → F) (x' - x₀) : F)) fun (x' : E) ↦ x' - x₀
simp_rw₁ :
  IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - 0) ((0 : (a : E) → F) (x' - x₀) : F)) fun (x' : E) ↦ x' - x₀
simp_rw₂ : IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀) (fun (x' : E) ↦ f x' - 0 - 0) fun (x' : E) ↦ x' - x₀
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x₀
have simp_rw₃ : IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀) (fun (x' : E) ↦ f x') fun (x' : E) ↦ x' - x₀
Tactic: simp_rw [hasFDerivWithinAt_iff_isLittleO,
    h.eq_zero_of_norm_pow_within hx₀ hn.ne_bot, zero_apply, sub_zero,
    h.trans_isLittleO ((isLittleO_pow_sub_sub x₀ hn).mono nhdsWithin_le_nhds)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (hypothesis)
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
n : ℕ
h : IsBigO (F := ℝ) (𝓝 x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n
hn : 1 < n
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x₀
have h₁ : IsBigO (F := ℝ) (𝓝[univ] x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n
Tactic: rw [← nhdsWithin_univ] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (hypothesis)
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
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s
have 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
Tactic: have := hf.isLittleO.add_isBigOWith (f'.isBigOWith_comp _ _) hK
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (hypothesis)
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
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s
have this₁ : ∀ᶠ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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‖
⊢ ∃ s ∈ 𝓝 x, LipschitzOnWith K f s
have 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
Tactic: rcases exists_nhds_square this with ⟨U, Uo, xU, hU⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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
have refine_1 : ∀ (ε : ℝ) (ε0 : 0 < ε), 0 ≤ C + ε
Tactic: refine le_of_forall_pos_le_add fun ε ε0 => opNorm_le_of_nhds_zero ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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 + ε
⊢ ‖f'‖ ≤ C
have refine_2 : ∀ (ε : ℝ) (ε0 : 0 < ε), ∀ᶠ (x : E) in 𝓝 0, norm.{u_3} (E := F) ((f' : (a : E) → F) x : F) ≤ (C + ε) * ‖x‖
Tactic: refine le_of_forall_pos_le_add fun ε ε0 => opNorm_le_of_nhds_zero ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, norm.{u_3} (E := F) ((f' : (a : E) → F) x : F) ≤ (C + ε) * ‖x‖
have 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‖
Tactic: rw [← map_add_left_nhds_zero x₀, eventually_map] at hlip
Cleared hypotheses: hlip, ε, ε0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, norm.{u_3} (E := F) ((f' : (a : E) → F) x : F) ≤ (C + ε) * ‖x‖
have 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‖
Tactic: filter_upwards [isLittleO_iff.1 (hasFDerivAt_iff_isLittleO_nhds_zero.1 hf) ε0, hlip] with y hy hyC
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (hypothesis)
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₀‖
⊢ norm.{u_3} (E := F) ((f' : (a : E) → F) y : F) ≤ (C + ε) * ‖y‖
have hyC₁ : ‖f (x₀ + y) - f x₀‖ ≤ C * ‖y‖
Tactic: rw [add_sub_cancel_left] at hyC
Cleared hypotheses: hyC
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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 : ℝ)
have refine : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
Tactic: refine hf.le_of_lip' C.coe_nonneg ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
have 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
Tactic: filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
have h₁ : ∀ a ∈ s, ‖f a - f x₀‖ ≤ (↑C : ℝ) * ‖a - x₀‖
Tactic: filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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₀‖
⊢ norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ C
have pos : ∀ (hf : DifferentiableAt 𝕜 f x₀), norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ C
Tactic: by_cases hf : DifferentiableAt 𝕜 f x₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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
⊢ norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ C
have neg : ∀ (hf : ¬DifferentiableAt 𝕜 f x₀), norm (E := E →L[𝕜] F) (fderiv 𝕜 f x₀) ≤ C
Tactic: by_cases hf : DifferentiableAt 𝕜 f x₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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
have neg : norm (E := E →L[𝕜] F) 0 ≤ C
Tactic: rw [fderiv_zero_of_not_differentiableAt hf]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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 : ℝ)
have refine : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
Tactic: refine norm_fderiv_le_of_lip' 𝕜 C.coe_nonneg ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
have 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
Tactic: filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
have h₁ : ∀ a ∈ s, ‖f a - f x₀‖ ≤ (↑C : ℝ) * ‖a - x₀‖
Tactic: filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (hypothesis)
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)
⊢ HasFDerivAt ((⇑L : (a : W) → W') ∘ f ∘ (⇑R : (a : V') → V)) (L ∘SL f' ∘SL R) z
have this : RingHomIsometric σ'
Tactic: have : RingHomIsometric σ' := .inv σ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (goal)
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 σ'
⊢ HasFDerivAt ((⇑L : (a : W) → W') ∘ f ∘ (⇑R : (a : V') → V)) (L ∘SL f' ∘SL R) z
have 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
Tactic: rw [hasFDerivAt_iff_isLittleO_nhds_zero] at ⊢ hf
Cleared hypotheses: hf, this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Basic (hypothesis)
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_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
have this₁ : 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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Bilinear (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ HasStrictFDerivAt b (h.deriv p) p
have simp : IsLittleO (E := G) (F := E × F) (𝓝 (p, p))
  (fun (p_1 : (E × F) × E × F) ↦
    HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G))
  fun (p : (E × F) × E × F) ↦ p.1 - p.2
Tactic: simp only [hasStrictFDerivAt_iff_isLittleO]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Bilinear (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ IsLittleO (E := G) (F := E × F) (𝓝 (p, p))
    (fun (p_1 : (E × F) × E × F) ↦
      HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G))
    fun (p : (E × F) × E × F) ↦ p.1 - p.2
have simp : IsLittleO (α := (E × F) × E × F) (E := G) (F := E × F) (𝓝 0)
  ((fun (p_1 : (E × F) × E × F) ↦
      HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
    fun (x : (E × F) × E × F) ↦ (p, p) + x)
  ((fun (p : (E × F) × E × F) ↦ p.1 - p.2) ∘ fun (x : (E × F) × E × F) ↦ (p, p) + x)
Tactic: simp only [← map_add_left_nhds_zero (p, p), isLittleO_map]