-- 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
⊢ ∀ (x y : E),
    (fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }) (x + y) =
      (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

Tactic:
intros

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
x✝ y✝ : E
⊢ (fun x => { toFun := fun y => (f'' x) y, map_add' := ⋯, map_smul' := ⋯ }) (x✝ + y✝) =
    (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✝

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
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''‖ ⋯
hx : Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f' x' - f' x - f'' (x' - x)‖) (𝓝 x) (𝓝 0)
⊢ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f'R x' - f'R x - f''R (x' - x)‖) (𝓝 x) (𝓝 0)

Tactic:
exact hx

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
x : E
⊢ ∀ (x_1 y : E), (fun y => (f'' x) y) (x_1 + y) = (fun y => (f'' x) y) x_1 + (fun y => (f'' x) y) y

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
⊢ ∀ (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:
intros

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
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✝