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

Tactic:
have C := this.smul_isLittleO A

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 => (f'' w) v - (f'' v) w) =o[𝓝[>] 0] fun x => 1

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

Tactic:
ext h

Result:
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 - (f'' v) w) =
    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 • w + 2 • v)) + f (x + h • (w + v)) - f (x + h • (2 • w + v)) - f (x + h • (w + 2 • v)) -
        h ^ 2 • (f'' w) v)

Proof state:
case 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
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
h : ℝ
hpos : 0 < h
⊢ (1 / h ^ 2) • h ^ 2 = 1

Tactic:
field_simp

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
⊢ (fun x => (f'' w) v - (f'' v) w) =o[𝓝[>] 0] fun x => 1

Tactic:
have : (fun h : ℝ => 1 / h ^ 2) =O[𝓝[>] 0] fun h => 1 / h ^ 2 := isBigO_refl _ _

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
⊢ (fun x => (f'' w) v - (f'' v) w) =o[𝓝[>] 0] fun x => 1

Proof state:
case 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
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
h : ℝ
hpos : 0 < h
⊢ (1 / h ^ 2) • h ^ 2 • ((f'' w) v - (f'' v) w) = (f'' w) v - (f'' v) w

Tactic:
match_scalars <;> field_simp

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 => (1 / x ^ 2) • x ^ 2) =ᶠ[𝓝[>] 0] fun x => 1

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

Result:
case 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
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
h : ℝ
hpos : 0 < h
⊢ (1 / h ^ 2) • h ^ 2 = 1