-- Mathlib/Analysis/Calculus/ContDiff/RCLike.lean
theorem ContDiffAt.hasStrictFDerivAt' {f : E' → F'} {f' : E' →L[𝕂] F'} {x : E'}
    (hf : ContDiffAt 𝕂 n f x) (hf' : HasFDerivAt f f' x) (hn : 1 ≤ n) :
    HasStrictFDerivAt f f' x

Proof state:
case intro.intro.intro
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
u : Set E'
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1) f p u
H : u ∈ 𝓝 x
this : HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕂 E' F') (p x 1)) x
⊢ HasStrictFDerivAt f f' x

Tactic:
rwa [hf'.unique this.hasFDerivAt]

Result:
no goals

Proof state:
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
⊢ HasStrictFDerivAt f f' x

Tactic:
rcases hf.of_le hn 1 le_rfl with ⟨u, H, p, hp⟩

Result:
case intro.intro.intro
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
u : Set E'
H : u ∈ 𝓝[insert x univ] x
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1) f p u
⊢ HasStrictFDerivAt f f' x

Proof state:
case intro.intro.intro
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
u : Set E'
H : u ∈ 𝓝[insert x univ] x
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1) f p u
⊢ HasStrictFDerivAt f f' x

Tactic:
simp only [nhdsWithin_univ, mem_univ, insert_eq_of_mem] at H

Result:
case intro.intro.intro
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
u : Set E'
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1) f p u
H : u ∈ 𝓝 x
⊢ HasStrictFDerivAt f f' x

Proof state:
case intro.intro.intro
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
u : Set E'
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1) f p u
H : u ∈ 𝓝 x
⊢ HasStrictFDerivAt f f' x

Tactic:
have := hp.hasStrictFDerivAt le_rfl H

Result:
case intro.intro.intro
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
u : Set E'
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1) f p u
H : u ∈ 𝓝 x
this : HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕂 E' F') (p x 1)) x
⊢ HasStrictFDerivAt f f' x