awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
have h : Eq.{u_2 + 1} (α := ℝ → F)
  (fun (h : ℝ) ↦
    HPow.hPow (β := ℕ) h 2 •
      HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
        ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
  fun (x_1 : ℝ) ↦
  f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + x_1 • (v + w)) -
          f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 v + w)) -
        f (x + x_1 • (v + HSMul.hSMul (α := ℕ) 2 w)) -
      HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
        ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
    (f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 w + HSMul.hSMul (α := ℕ) 2 v)) + f (x + x_1 • (w + v)) -
          f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 w + v)) -
        f (x + x_1 • (w + HSMul.hSMul (α := ℕ) 2 v)) -
      HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
        ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
Tactic: convert!
      (s_conv.isLittleO_alternate_sum_square hf xs hx h4v h4w).sub
        (s_conv.isLittleO_alternate_sum_square hf xs hx h4w h4v) using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
⊢ Eq.{u_2 + 1} (α := ℝ → F)
    (fun (h : ℝ) ↦
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x_1 : ℝ) ↦
    f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + x_1 • (v + w)) -
            f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + x_1 • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
      (f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 w + HSMul.hSMul (α := ℕ) 2 v)) + f (x + x_1 • (w + v)) -
            f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 w + v)) -
          f (x + x_1 • (w + HSMul.hSMul (α := ℕ) 2 v)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
          ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
have h : ∀ (h : ℝ),
  HPow.hPow (β := ℕ) h 2 •
      HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
        ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
    f (x + h • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + h • (v + w)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + h • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
      (f (x + h • (HSMul.hSMul (α := ℕ) 2 w + HSMul.hSMul (α := ℕ) 2 v)) + f (x + h • (w + v)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 w + v)) -
          f (x + h • (w + HSMul.hSMul (α := ℕ) 2 v)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
Tactic: ext h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
h : ℝ
⊢ HPow.hPow (β := ℕ) h 2 •
      HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
        ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
    f (x + h • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + h • (v + w)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + h • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
      (f (x + h • (HSMul.hSMul (α := ℕ) 2 w + HSMul.hSMul (α := ℕ) 2 v)) + f (x + h • (w + v)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 w + v)) -
          f (x + h • (w + HSMul.hSMul (α := ℕ) 2 v)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
have h₁ : HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F) -
    HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
  f (x + (h • v + h • w)) + f (x + (h • HSMul.hSMul (α := ℕ) 2 v + h • HSMul.hSMul (α := ℕ) 2 w)) -
          f (x + (h • w + h • HSMul.hSMul (α := ℕ) 2 v)) -
        f (x + (h • v + h • HSMul.hSMul (α := ℕ) 2 w)) -
      HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
        ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
    (f (x + (h • v + h • w)) + f (x + (h • HSMul.hSMul (α := ℕ) 2 v + h • HSMul.hSMul (α := ℕ) 2 w)) -
          f (x + (h • v + h • HSMul.hSMul (α := ℕ) 2 w)) -
        f (x + (h • w + h • HSMul.hSMul (α := ℕ) 2 v)) -
      HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
Tactic: simp only [add_comm, smul_add, smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
⊢ Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
    ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
have A : IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
  (fun (h : ℝ) ↦
    HPow.hPow (β := ℕ) h 2 •
      HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
        ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
  fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
Tactic: have A : (fun h : ℝ => h ^ 2 • (f'' w v - f'' v w)) =o[𝓝[>] 0] fun h => h ^ 2 := by
    convert!
      (s_conv.isLittleO_alternate_sum_square hf xs hx h4v h4w).sub
        (s_conv.isLittleO_alternate_sum_square hf xs hx h4w h4v) using 1
    ext h
    simp only [add_comm, smul_add, smul_sub]
    abel
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
        ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x : ℝ) ↦ 1
have this : IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2) fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2
Tactic: have : (fun h : ℝ => 1 / h ^ 2) =O[𝓝[>] 0] fun h => 1 / h ^ 2 := isBigO_refl _ _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
this :
  IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2) fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2
C :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      (1 / HPow.hPow (β := ℕ) x 2) •
        HPow.hPow (β := ℕ) x 2 •
          HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x : ℝ) ↦ (1 / HPow.hPow (β := ℕ) x 2) • HPow.hPow (β := ℕ) x 2
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
        ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x : ℝ) ↦ 1
have apply : EventuallyEq.{0, u_2} (β := F) (𝓝[>] 0)
  (fun (x : ℝ) ↦
    (1 / HPow.hPow (β := ℕ) x 2) •
      HPow.hPow (β := ℕ) x 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
  fun (x : ℝ) ↦
  HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
    ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
Tactic: apply C.congr' _ _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
this :
  IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2) fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2
C :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      (1 / HPow.hPow (β := ℕ) x 2) •
        HPow.hPow (β := ℕ) x 2 •
          HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x : ℝ) ↦ (1 / HPow.hPow (β := ℕ) x 2) • HPow.hPow (β := ℕ) x 2
apply :
  EventuallyEq.{0, u_2} (β := F) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      (1 / HPow.hPow (β := ℕ) x 2) •
        HPow.hPow (β := ℕ) x 2 •
          HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x : ℝ) ↦
    HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
      ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
        ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x : ℝ) ↦ 1
have apply₁ : EventuallyEq (β := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (1 / HPow.hPow (β := ℕ) x 2) • HPow.hPow (β := ℕ) x 2) fun (x : ℝ) ↦ 1
Tactic: apply C.congr' _ _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
this :
  IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2) fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2
C :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      (1 / HPow.hPow (β := ℕ) x 2) •
        HPow.hPow (β := ℕ) x 2 •
          HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x : ℝ) ↦ (1 / HPow.hPow (β := ℕ) x 2) • HPow.hPow (β := ℕ) x 2
⊢ EventuallyEq.{0, u_2} (β := F) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      (1 / HPow.hPow (β := ℕ) x 2) •
        HPow.hPow (β := ℕ) x 2 •
          HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x : ℝ) ↦
    HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
      ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ) (Ioi 0) a →
    (1 / HPow.hPow (β := ℕ) a 2) •
        HPow.hPow (β := ℕ) a 2 •
          HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
      HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
        ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
Tactic: filter_upwards [self_mem_nhdsWithin]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
this :
  IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2) fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2
C :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      (1 / HPow.hPow (β := ℕ) x 2) •
        HPow.hPow (β := ℕ) x 2 •
          HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x : ℝ) ↦ (1 / HPow.hPow (β := ℕ) x 2) • HPow.hPow (β := ℕ) x 2
h : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) h →
    (1 / HPow.hPow (β := ℕ) h 2) •
        HPow.hPow (β := ℕ) h 2 •
          HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
      HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
        ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
have h₁ : ∀ (hpos : 0 < h),
  (1 / HPow.hPow (β := ℕ) h 2) •
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
    HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
      ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
Tactic: (hpos : 0 < h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
this :
  IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2) fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2
C :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      (1 / HPow.hPow (β := ℕ) x 2) •
        HPow.hPow (β := ℕ) x 2 •
          HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x : ℝ) ↦ (1 / HPow.hPow (β := ℕ) x 2) • HPow.hPow (β := ℕ) x 2
h : ℝ
hpos : 0 < h
⊢ (1 / HPow.hPow (β := ℕ) h 2) •
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
    HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
      ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
have match_scalars : 1 / HPow.hPow (β := ℕ) h 2 * (HPow.hPow (β := ℕ) h 2 * 1) = 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
this :
  IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2) fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2
C :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      (1 / HPow.hPow (β := ℕ) x 2) •
        HPow.hPow (β := ℕ) x 2 •
          HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x : ℝ) ↦ (1 / HPow.hPow (β := ℕ) x 2) • HPow.hPow (β := ℕ) x 2
h : ℝ
hpos : 0 < h
match_scalars : 1 / HPow.hPow (β := ℕ) h 2 * (HPow.hPow (β := ℕ) h 2 * 1) = 1
⊢ (1 / HPow.hPow (β := ℕ) h 2) •
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
    HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
      ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
have match_scalars₁ : 1 / HPow.hPow (β := ℕ) h 2 * (HPow.hPow (β := ℕ) h 2 * -1) = -1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
this :
  IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2) fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2
C :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      (1 / HPow.hPow (β := ℕ) x 2) •
        HPow.hPow (β := ℕ) x 2 •
          HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x : ℝ) ↦ (1 / HPow.hPow (β := ℕ) x 2) • HPow.hPow (β := ℕ) x 2
h : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) h → (1 / HPow.hPow (β := ℕ) h 2) • HPow.hPow (β := ℕ) h 2 = 1
have h₁ : ∀ (hpos : 0 < h), (1 / HPow.hPow (β := ℕ) h 2) • HPow.hPow (β := ℕ) h 2 = 1
Tactic: (hpos : 0 < h)