-- Mathlib/Analysis/Calculus/Implicit.lean
theorem tendsto_implicitFunction (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) {α : Type*}
    {l : Filter α} {g₁ : α → F} {g₂ : α → ker f'} (h₁ : Tendsto g₁ l (𝓝 <| f a))
    (h₂ : Tendsto g₂ l (𝓝 0)) :
    Tendsto (fun t => hf.implicitFunction f f' hf' (g₁ t) (g₂ t)) l (𝓝 a)

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → ↥(LinearMap.ker f')
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
⊢ Tendsto (fun t => implicitFunction f f' hf hf' (g₁ t) (g₂ t)) l (𝓝 a)

Tactic:
refine ((hf.implicitToPartialHomeomorph f f' hf').tendsto_symm
  (hf.mem_implicitToPartialHomeomorph_source hf')).comp ?_

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → ↥(LinearMap.ker f')
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
⊢ Tendsto (fun t => (g₁ t, g₂ t)) l (𝓝 (↑(implicitToPartialHomeomorph f f' hf hf') a))

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → ↥(LinearMap.ker f')
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
⊢ Tendsto (fun t => (g₁ t, g₂ t)) l (𝓝 (f a, 0))

Tactic:
exact h₁.prod_mk_nhds h₂

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → ↥(LinearMap.ker f')
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
⊢ Tendsto (fun t => (g₁ t, g₂ t)) l (𝓝 (↑(implicitToPartialHomeomorph f f' hf hf') a))

Tactic:
rw [implicitToPartialHomeomorph_self]

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → ↥(LinearMap.ker f')
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
⊢ Tendsto (fun t => (g₁ t, g₂ t)) l (𝓝 (f a, 0))