-- 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
m✝ : ℝ
x✝ : E
⊢ { toFun := fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun (m✝ • x✝) =
    (RingHom.id ℝ) m✝ •
      { toFun := fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun x✝

Tactic:
ext

Result:
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
m✝ : ℝ
x✝¹ x✝ : E
⊢ ({ toFun := fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun (m✝ • x✝¹))
      x✝ =
    ((RingHom.id ℝ) m✝ •
        { toFun := fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun x✝¹)
      x✝

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

Tactic:
let _ : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul

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

Tactic:
let _ : LinearMap.CompatibleSMul E F ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul

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
⊢ (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
x : E
⊢ ∀ (m : ℝ) (x_1 : E),
    { toFun := fun y => (f'' x) y, map_add' := ⋯ }.toFun (m • x_1) =
      (RingHom.id ℝ) m • { toFun := fun y => (f'' x) y, map_add' := ⋯ }.toFun x_1

Tactic:
simp

Result:
no goals