-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
theorem Convex.second_derivative_within_at_symmetric_of_mem_interior {v w : E}
    (h4v : x + (4 : ℝ) • v ∈ interior s) (h4w : x + (4 : ℝ) • w ∈ interior s) :
    f'' w v = f'' v w

Proof state:
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 : (fun h => h ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun h => h ^ 2
B : (fun x => (f'' w) v - (f'' v) w) =o[𝓝[>] 0] fun x => 1
⊢ (f'' w) v = (f'' v) w

Tactic:
simpa only [sub_eq_zero] using isLittleO_const_const_iff.1 B

Result:
no goals

Proof state:
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 : (fun h => h ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[>] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun x => (1 / x ^ 2) • x ^ 2
⊢ (fun x => (f'' w) v - (f'' v) w) =o[𝓝[>] 0] fun x => 1

Tactic:
apply C.congr' _ _

Result:
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 : (fun h => h ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[>] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun x => (1 / x ^ 2) • x ^ 2
⊢ (fun x => (1 / x ^ 2) • x ^ 2 • ((f'' w) v - (f'' v) w)) =ᶠ[𝓝[>] 0] fun x => (f'' w) v - (f'' v) w

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 : (fun h => h ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun h => h ^ 2
this : (fun h => 1 / h ^ 2) =O[𝓝[>] 0] fun h => 1 / h ^ 2
C : (fun x => (1 / x ^ 2) • x ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun x => (1 / x ^ 2) • x ^ 2
⊢ (fun x => (1 / x ^ 2) • x ^ 2) =ᶠ[𝓝[>] 0] fun x => 1

Proof state:
case h.e'_7.h
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
h : ℝ
⊢ h ^ 2 • (f'' w) v - h ^ 2 • (f'' v) w =
    f (x + (h • v + h • w)) + f (x + (h • 2 • v + h • 2 • w)) - f (x + (h • w + h • 2 • v)) -
          f (x + (h • v + h • 2 • w)) -
        h ^ 2 • (f'' v) w -
      (f (x + (h • v + h • w)) + f (x + (h • 2 • v + h • 2 • w)) - f (x + (h • v + h • 2 • w)) -
          f (x + (h • w + h • 2 • v)) -
        h ^ 2 • (f'' w) v)

Tactic:
abel

Result:
no goals