-- 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 𝕜
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'' v) w = (f'' w) v

Tactic:
let f''Rl : E →ₗ[ℝ] E →ₗ[ℝ] F :=
{ toFun := fun x ↦
    { toFun := fun y ↦ f'' x y
      map_add' := by simp
      map_smul' := by simp }
  map_add' := by intros; ext; simp
  map_smul' := by intros; ext; simp }

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'' 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' := ⋯ }
f''R : E →L[ℝ] E →L[ℝ] F := f''Rl.mkContinuous₂ ‖f''‖ ⋯
⊢ (f'' v) w = (f'' w) v

Tactic:
have : HasFDerivAt f'R f''R x := by
  simp only [hasFDerivAt_iff_tendsto] at hx ⊢
  exact hx

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''‖ ⋯
this : HasFDerivAt f'R f''R x
⊢ (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''Rl x) y‖ ≤ ‖f''‖ * ‖x‖ * ‖y‖

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk, f''Rl]

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' := ⋯ }
x y : E
⊢ ‖(f'' x) y‖ ≤ ‖f''‖ * ‖x‖ * ‖y‖

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)
⊢ ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y

Tactic:
filter_upwards [hf] with y hy using HasFDerivAt.restrictScalars ℝ hy

Result:
no goals