awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 :
  ∀ (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))
⊢ 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:
ext h
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : ℝ
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))
⊢ 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:
simp only [add_comm, smul_add, smul_sub]

Premises used: add_comm, smul_sub, smul_add
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : ℝ
⊢ 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:
abel
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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

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
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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
⊢ 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 _ _
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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)
apply₁ :
  EventuallyEq (β := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (1 / HPow.hPow (β := ℕ) x 2) • HPow.hPow (β := ℕ) x 2) fun (x : ℝ) ↦ 1
⊢ 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

Tactic:
apply C.congr' _ _

Premises used: Asymptotics.IsLittleO.congr'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 :
  ∀ (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)
⊢ 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:
filter_upwards [self_mem_nhdsWithin]

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : ℝ
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)
⊢ 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)

Tactic:
(hpos : 0 < h)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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
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)

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 * 1) = 1

Tactic:
field
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 * -1) = -1

Tactic:
field
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : ℝ
h₁ : ∀ (hpos : 0 < h), (1 / HPow.hPow (β := ℕ) h 2) • HPow.hPow (β := ℕ) h 2 = 1
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) h → (1 / HPow.hPow (β := ℕ) h 2) • HPow.hPow (β := ℕ) h 2 = 1

Tactic:
(hpos : 0 < h)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : ∀ (h : ℝ) (hpos : 0 < h), (1 / HPow.hPow (β := ℕ) h 2) • HPow.hPow (β := ℕ) h 2 = 1
⊢ EventuallyEq (β := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (1 / HPow.hPow (β := ℕ) x 2) • HPow.hPow (β := ℕ) x 2) fun (x : ℝ) ↦ 1

Tactic:
filter_upwards [self_mem_nhdsWithin] with h (hpos : 0 < h)

Premises used: self_mem_nhdsWithin