-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
theorem second_derivative_symmetric_of_eventually [IsRCLikeNormedField 𝕜]
    {f' : E → E →L[𝕜] F} {x : E}
    {f'' : E →L[𝕜] E →L[𝕜] F} (hf : ∀ᶠ y in 𝓝 x, HasFDerivAt f (f' y) y)
    (hx : HasFDerivAt f' f'' x) (v w : E) : f'' v w = f'' w v

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ (f'' v) w = (f'' w) v

Tactic:
let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ (f'' v) w = (f'' w) v

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x✝⁵ : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x✝⁵, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x✝⁵
v w : E
x✝⁴ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝³ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝² : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
x✝¹ : LinearMap.CompatibleSMul E F ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
x✝ : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
f'R : E → E →L[ℝ] F := fun x => ContinuousLinearMap.restrictScalars ℝ (f' x)
hfR : ∀ᶠ (y : E) in 𝓝 x✝⁵, HasFDerivAt f (f'R y) y
f''Rl : E →ₗ[ℝ] E →ₗ[ℝ] F :=
  { toFun := fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
x y : E
⊢ ‖(f'' x) y‖ ≤ ‖f''‖ * ‖x‖ * ‖y‖

Tactic:
exact ContinuousLinearMap.le_opNorm₂ f'' x y

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x✝⁶ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝⁵ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝⁴ : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
x✝³ : LinearMap.CompatibleSMul E F ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
x✝² : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
f'R : E → E →L[ℝ] F := fun x => ContinuousLinearMap.restrictScalars ℝ (f' x)
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
x✝¹ y✝ x✝ : E
⊢ ((fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }) (x✝¹ + y✝)) x✝ =
    ((fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }) x✝¹ +
        (fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }) y✝)
      x✝

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x✝⁴ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝³ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝² : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
x✝¹ : LinearMap.CompatibleSMul E F ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
x✝ : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
f'R : E → E →L[ℝ] F := fun x => ContinuousLinearMap.restrictScalars ℝ (f' x)
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
f''Rl : E →ₗ[ℝ] E →ₗ[ℝ] F :=
  { toFun := fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
⊢ (f'' v) w = (f'' w) v

Tactic:
let f''R : E →L[ℝ] E →L[ℝ] F := by
  refine LinearMap.mkContinuous₂ f''Rl (‖f''‖) (fun x y ↦ ?_)
  simp only [LinearMap.coe_mk, AddHom.coe_mk, f''Rl]
  exact ContinuousLinearMap.le_opNorm₂ f'' x y

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x✝⁴ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝³ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝² : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
x✝¹ : LinearMap.CompatibleSMul E F ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
x✝ : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
f'R : E → E →L[ℝ] F := fun x => ContinuousLinearMap.restrictScalars ℝ (f' x)
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
f''Rl : E →ₗ[ℝ] E →ₗ[ℝ] F :=
  { toFun := fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
f''R : E →L[ℝ] E →L[ℝ] F := f''Rl.mkContinuous₂ ‖f''‖ ⋯
⊢ (f'' v) w = (f'' w) v