Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: case e'_7
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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 + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : 1 / 2 ∈ Ioc 0 1
B : 1 / 2 ∈ Icc 0 1
h2v2w : x + 2 • v + 2 • w ∈ interior s
h2vww : x + (2 • v + w) + w ∈ interior s
h2v : x + 2 • v ∈ interior s
h2w : x + 2 • w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (2 • v + w) ∈ interior s
hvww : x + (v + w) + w ∈ interior s
TA1 :
  (fun h ↦
      f (x + h • (2 • v + w) + h • w) - f (x + h • (2 • v + w)) - h • (f' x) w - h ^ 2 • (f'' (2 • v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2
TA2 :
  (fun h ↦
      f (x + h • (v + w) + h • w) - f (x + h • (v + w)) - h • (f' x) w - h ^ 2 • (f'' (v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2
h : ℝ
⊢ f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) -
      h ^ 2 • (f'' v) w =
    f (x + h • (2 • v + w) + h • w) - f (x + h • (2 • v + w)) - h • (f' x) w - h ^ 2 • (f'' (2 • v + w)) w -
        (h ^ 2 / 2) • (f'' w) w -
      (f (x + h • (v + w) + h • w) - f (x + h • (v + w)) - h • (f' x) w - h ^ 2 • (f'' (v + w)) w -
        (h ^ 2 / 2) • (f'' w) w)

Tactic:
simp only [two_smul, smul_add, ← add_assoc, map_add,
    add_apply]

Goal state after:
case e'_7
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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 + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : 1 / 2 ∈ Ioc 0 1
B : 1 / 2 ∈ Icc 0 1
h2v2w : x + 2 • v + 2 • w ∈ interior s
h2vww : x + (2 • v + w) + w ∈ interior s
h2v : x + 2 • v ∈ interior s
h2w : x + 2 • w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (2 • v + w) ∈ interior s
hvww : x + (v + w) + w ∈ interior s
TA1 :
  (fun h ↦
      f (x + h • (2 • v + w) + h • w) - f (x + h • (2 • v + w)) - h • (f' x) w - h ^ 2 • (f'' (2 • v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2
TA2 :
  (fun h ↦
      f (x + h • (v + w) + h • w) - f (x + h • (v + w)) - h • (f' x) w - h ^ 2 • (f'' (v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2
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) -
      h ^ 2 • (f'' v) w =
    f (x + h • v + h • v + h • w + h • w) - f (x + h • v + h • v + h • w) - h • (f' x) w -
          (h ^ 2 • (f'' v) w + h ^ 2 • (f'' v) w + h ^ 2 • (f'' w) w) -
        (h ^ 2 / 2) • (f'' w) w -
      (f (x + h • v + h • w + h • w) - f (x + h • v + h • w) - h • (f' x) w - (h ^ 2 • (f'' v) w + h ^ 2 • (f'' w) w) -
        (h ^ 2 / 2) • (f'' w) w)