-- 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 : 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 : ℝ
⊢ 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 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) -
      (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))
have h₁ : f (x + h • v + h • v + h • w + h • w) + f (x + h • v + h • w) - f (x + h • v + h • v + h • w) -
      f (x + h • v + h • w + h • 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 • v + h • w + h • w) - f (x + h • v + h • v + h • 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 : E →L[ℝ] F) : (a : E) → F) w : F) +
            HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
              ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) +
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
            ((((f'' : (a : E) → E →L[ℝ] F) 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) -
    (f (x + h • v + h • w + h • w) - f (x + h • v + h • 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 : E →L[ℝ] F) : (a : E) → F) w : F) +
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
            ((((f'' : (a : E) → E →L[ℝ] F) 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))
Tactic: simp only [two_smul, smul_add, ← add_assoc, map_add,
    ContinuousLinearMap.add_apply]