-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffWithinAt.hasFDerivWithinAt_nhds {f : E → F → G} {g : E → F} {t : Set F} (hn : n ≠ ∞)
    {x₀ : E} (hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀))
    (hg : ContDiffWithinAt 𝕜 n g s x₀) (hgt : t ∈ 𝓝[g '' s] g x₀) :
    ∃ v ∈ 𝓝[insert x₀ s] x₀, v ⊆ insert x₀ s ∧ ∃ f' : E → F →L[𝕜] G,
      (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧
        ContDiffWithinAt 𝕜 n (fun x => f' x) s x₀

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
n : WithTop ℕ∞
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀)
⊢ ∃ v ∈ 𝓝[insert x₀ s] x₀,
    v ⊆ insert x₀ s ∧
      ∃ f', (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧ ContDiffWithinAt 𝕜 n (fun x => f' x) s x₀

Tactic:
obtain ⟨v, hv, hvs, f_an, f', hvf', hf'⟩ :=
  (contDiffWithinAt_succ_iff_hasFDerivWithinAt' hn).mp hf

Result:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
n : WithTop ℕ∞
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
⊢ ∃ v ∈ 𝓝[insert x₀ s] x₀,
    v ⊆ insert x₀ s ∧
      ∃ f', (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧ ContDiffWithinAt 𝕜 n (fun x => f' x) s x₀

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
n : WithTop ℕ∞
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀) ≤ 𝓝[insert x₀ s ×ˢ t] (x₀, g x₀)
v : Set (E × F)
hv : 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀) ≤ 𝓝[v] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
this : (x₀, g x₀) ∈ v
⊢ 𝓝[(fun x => (id x, g x)) '' s] (id x₀, g x₀) ≤ 𝓝[v] (id x₀, g x₀)

Tactic:
exact (hst.trans <| nhdsWithin_mono _ <| subset_insert _ _).trans hv

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
n : WithTop ℕ∞
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
z : E
hz : z ∈ (fun z => (z, g z)) ⁻¹' v ∩ insert x₀ s
⊢ HasFDerivWithinAt (f z) ((fun z => (f' (z, g z)).comp (ContinuousLinearMap.inr 𝕜 E F)) z) t (g z)

Tactic:
have := hvf' (z, g z) hz.1

Result:
case intro.intro.intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
n : WithTop ℕ∞
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
z : E
hz : z ∈ (fun z => (z, g z)) ⁻¹' v ∩ insert x₀ s
this : HasFDerivWithinAt (uncurry f) (f' (z, g z)) (insert x₀ s ×ˢ t) (z, g z)
⊢ HasFDerivWithinAt (f z) ((fun z => (f' (z, g z)).comp (ContinuousLinearMap.inr 𝕜 E F)) z) t (g z)