-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
theorem ContDiffAt.isSymmSndFDerivAt {n : WithTop ℕ∞}
    (hf : ContDiffAt 𝕜 n f x) (hn : minSmoothness 𝕜 2 ≤ n) : IsSymmSndFDerivAt 𝕜 f x

Proof state:
case pos
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
⊢ ((fderiv 𝕜 (fderiv 𝕜 f) x) v) w = ((fderiv 𝕜 (fderiv 𝕜 f) x) w) v

Tactic:
apply second_derivative_symmetric_of_eventually (f := f) (f' := fderiv 𝕜 f) (x := x)

Result:
case pos.hf
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
⊢ ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (fderiv 𝕜 f y) y

case pos.hx
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
⊢ HasFDerivAt (fderiv 𝕜 f) (fderiv 𝕜 (fderiv 𝕜 f) x) x

Proof state:
case pos.hf
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
⊢ ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (fderiv 𝕜 f y) y

Tactic:
obtain ⟨u, hu, h'u⟩ : ∃ u ∈ 𝓝 x, ContDiffOn 𝕜 2 f u :=
  (hf.of_le hn).contDiffOn (m := 2) le_minSmoothness (by simp)

Result:
case pos.hf.intro.intro
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
u : Set E
hu : u ∈ 𝓝 x
h'u : ContDiffOn 𝕜 2 f u
⊢ ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (fderiv 𝕜 f y) y

Proof state:
case pos
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
⊢ IsSymmSndFDerivAt 𝕜 f x

Tactic:
intro v w

Result:
case pos
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
⊢ ((fderiv 𝕜 (fderiv 𝕜 f) x) v) w = ((fderiv 𝕜 (fderiv 𝕜 f) x) 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
⊢ ContDiffAt 𝕜 1 (fderiv 𝕜 f) x

Tactic:
exact hf.fderiv_right (le_minSmoothness.trans hn)

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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
⊢ IsSymmSndFDerivAt 𝕜 f x

Tactic:
by_cases h : IsRCLikeNormedField 𝕜

Result:
case pos
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
⊢ IsSymmSndFDerivAt 𝕜 f x

case neg
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : ¬IsRCLikeNormedField 𝕜
⊢ IsSymmSndFDerivAt 𝕜 f x

Proof state:
case neg
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
h : ¬IsRCLikeNormedField 𝕜
hn : n = ω
⊢ IsSymmSndFDerivAt 𝕜 f x

Tactic:
apply ContDiffAt.isSymmSndFDerivAt_of_omega

Result:
case neg.hf
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
h : ¬IsRCLikeNormedField 𝕜
hn : n = ω
⊢ ContDiffAt 𝕜 ω f 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
⊢ DifferentiableAt 𝕜 (fderiv 𝕜 f) x

Tactic:
apply ContDiffAt.differentiableAt _ le_rfl

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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
⊢ ContDiffAt 𝕜 1 (fderiv 𝕜 f) 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v✝ w : E
u : Set E
hu : u ∈ 𝓝 x
h'u : ContDiffOn 𝕜 2 f u
v : Set E
vu : v ⊆ u
v_open : IsOpen v
xv : x ∈ v
y : E
hy : y ∈ v
this : ContDiffAt 𝕜 2 f y
⊢ DifferentiableAt 𝕜 f y

Tactic:
exact this.differentiableAt one_le_two

Result:
no goals

Proof state:
case pos.hx
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
this : DifferentiableAt 𝕜 (fderiv 𝕜 f) x
⊢ HasFDerivAt (fderiv 𝕜 f) (fderiv 𝕜 (fderiv 𝕜 f) x) x

Tactic:
exact DifferentiableAt.hasFDerivAt this

Result:
no goals

Proof state:
case neg
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : ¬IsRCLikeNormedField 𝕜
⊢ IsSymmSndFDerivAt 𝕜 f x

Tactic:
simp only [minSmoothness, h, ↓reduceIte, top_le_iff] at hn

Result:
case neg
𝕜 : 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
x : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕜 n f x
h : ¬IsRCLikeNormedField 𝕜
hn : n = ω
⊢ IsSymmSndFDerivAt 𝕜 f x