-- 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 : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (HSMul.hSMul (α := ℕ) 2 v + w) ∈ interior s
hvww : x + (v + w) + w ∈ interior s
TA1 :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w) + h • w) - f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
            HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
            ((((f'' : (a : E) → E →L[ℝ] F) (HSMul.hSMul (α := ℕ) 2 v + w) : E →L[ℝ] F) : (a : E) → F) w : F) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2 / 2)
          ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
TA2 :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (v + w) + h • w) - f (x + h • (v + w)) - HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
            ((((f'' : (a : E) → E →L[ℝ] F) (v + w) : E →L[ℝ] F) : (a : E) → F) w : F) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2 / 2)
          ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
h :
  Eq.{u_2 + 1} (α := ℝ → F)
    (fun (h : ℝ) ↦
      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))
    fun (x_1 : ℝ) ↦
    f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 v + w) + x_1 • w) - f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 v + w)) -
            HSMul.hSMul (β := F) x_1 ((f' x : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
            ((((f'' : (a : E) → E →L[ℝ] F) (HSMul.hSMul (α := ℕ) 2 v + w) : E →L[ℝ] F) : (a : E) → F) w : F) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2 / 2)
          ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F) -
      (f (x + x_1 • (v + w) + x_1 • w) - f (x + x_1 • (v + w)) - HSMul.hSMul (β := F) x_1 ((f' x : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
            ((((f'' : (a : E) → E →L[ℝ] F) (v + w) : E →L[ℝ] F) : (a : E) → F) w : F) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2 / 2)
          ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F))
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      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))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2

Tactic:
convert! TA1.sub TA2 using 1

Premises used: Asymptotics.IsLittleO.sub