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

Tactic:
have : DifferentiableAt 𝕜 (fderiv 𝕜 f) x := by
  apply ContDiffAt.differentiableAt _ le_rfl
  exact hf.fderiv_right (le_minSmoothness.trans hn)

Result:
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

Proof state:
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

Tactic:
rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, xv⟩

Result:
case pos.hf.intro.intro.intro.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
v : Set E
vu : v ⊆ u
v_open : IsOpen v
xv : x ∈ v
⊢ ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (fderiv 𝕜 f y) y

Proof state:
case pos.hf.intro.intro.intro.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
v : Set E
vu : v ⊆ u
v_open : IsOpen v
xv : x ∈ v
⊢ ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (fderiv 𝕜 f y) y

Tactic:
filter_upwards [v_open.mem_nhds xv] with y hy

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
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
⊢ HasFDerivAt f (fderiv 𝕜 f y) y

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
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 : DifferentiableAt 𝕜 f y
⊢ HasFDerivAt f (fderiv 𝕜 f y) y

Tactic:
exact DifferentiableAt.hasFDerivAt this

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
h : IsRCLikeNormedField 𝕜
v w : E
⊢ 2 = ∞ → minSmoothness 𝕜 2 = ω

Tactic:
simp

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
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
⊢ HasFDerivAt f (fderiv 𝕜 f y) y

Tactic:
have : DifferentiableAt 𝕜 f y := by
  have := (h'u.mono vu y hy).contDiffAt (v_open.mem_nhds hy)
  exact this.differentiableAt one_le_two

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
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 : DifferentiableAt 𝕜 f y
⊢ HasFDerivAt f (fderiv 𝕜 f y) 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
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
⊢ DifferentiableAt 𝕜 f y

Tactic:
have := (h'u.mono vu y hy).contDiffAt (v_open.mem_nhds hy)

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

Proof state:
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

Tactic:
simpa [hn] using hf

Result:
no goals