awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
ψ : F → G → E
h : ∀ᶠ (x : E) in 𝓝 φ.pt, ψ (φ.leftFun x) (φ.rightFun x) = x
⊢ Function.uncurry ψ =ᶠ[𝓝 (φ.prodFun φ.pt)] Function.uncurry φ.implicitFunction

Tactic:
HasStrictFDerivAt.localInverse_unique _ h

Premises used: ImplicitFunctionData.implicitFunction, setOf, Filter.EventuallyEq, HasStrictFDerivAt.localInverse, OpenPartialHomeomorph.toFun', HasStrictFDerivAt.localInverse_unique
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
x : E
⊢ ((↑(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker) : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) x).1 = f x

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
y : E
⊢ (↑(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker) : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) y =
    (f y,
      (Classical.choose (p := fun (x : E →L[𝕜] ↥(↑f' : E →ₗ[𝕜] F).ker) ↦
            ∀ (x_1 : ↥(↑f' : E →ₗ[𝕜] F).ker), (x : (a : E) → ↥(↑f' : E →ₗ[𝕜] F).ker) (↑x_1 : E) = x_1) hker :
          (a : E) → ↥(↑f' : E →ₗ[𝕜] F).ker)
        (y - a))

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
y : ↥(↑f' : E →ₗ[𝕜] F).ker
⊢ (↑(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker) : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) ((↑y : E) + a) =
    (f ((↑y : E) + a), y)

Tactic:
simp only [implicitToOpenPartialHomeomorphOfComplemented_apply, add_sub_cancel_right,
    Classical.choose_spec hker]

Premises used: Classical.choose_spec, add_sub_cancel_right, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
⊢ (↑(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker) : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) a = (f a, 0)

Tactic:
simp [hf.implicitToOpenPartialHomeomorphOfComplemented_apply]

Premises used: HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
⊢ a ∈ (implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).source

Tactic:
ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source _

Premises used: Set.Mem, ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
⊢ (f a, 0) ∈ (implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).target

Tactic:
simpa only [implicitToOpenPartialHomeomorphOfComplemented_self] using
    (hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker).map_source <|
      hf.mem_implicitToOpenPartialHomeomorphOfComplemented_source hf' hker

Premises used: HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_source, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_self, OpenPartialHomeomorph.map_source
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
⊢ ∀ᶠ (p : Prod.{u_3, u_2} F ↥(↑f' : E →ₗ[𝕜] F).ker) in 𝓝 (f a, 0),
    f (implicitFunctionOfComplemented f f' hf hf' hker p.1 p.2) = p.1

Tactic:
((hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker).eventually_right_inverse <|
        hf.mem_implicitToOpenPartialHomeomorphOfComplemented_target hf' hker).mono
    fun ⟨_, _⟩ h => congr_arg Prod.fst h

Premises used: _private.0.HasStrictFDerivAt.map_implicitFunctionOfComplemented_eq.match_1, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_target, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented, OpenPartialHomeomorph.eventually_right_inverse, Prod.fst, Filter.Eventually.mono, congr_arg, HasStrictFDerivAt.implicitFunctionOfComplemented, Eq, Prod.snd
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
⊢ ∀ᶠ (x : E) in 𝓝 a,
    implicitFunctionOfComplemented f f' hf hf' hker (f x)
        ((↑(implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker) : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) x).2 =
      x

Tactic:
(implicitFunctionDataOfComplemented f f' hf hf' hker).implicitFunction_apply_image

Premises used: HasStrictFDerivAt.implicitFunctionDataOfComplemented, HasStrictFDerivAt.implicitFunctionOfComplemented, ImplicitFunctionData.implicitFunction_apply_image
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
⊢ implicitFunctionOfComplemented f f' hf hf' hker (f a) 0 = a

Tactic:
simpa only [implicitToOpenPartialHomeomorphOfComplemented_self] using
      (hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker).left_inv
      (hf.mem_implicitToOpenPartialHomeomorphOfComplemented_source hf' hker)

Premises used: HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented, OpenPartialHomeomorph.left_inv, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_source, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_self
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
⊢ HasStrictFDerivAt
    (ImplicitFunctionData.implicitFunction (implicitFunctionDataOfComplemented f f' hf hf' hker)
      (ImplicitFunctionData.leftFun (implicitFunctionDataOfComplemented f f' hf hf' hker)
        (ImplicitFunctionData.pt (implicitFunctionDataOfComplemented f f' hf hf' hker))))
    (↑f' : E →ₗ[𝕜] F).ker.subtypeL
    (ImplicitFunctionData.rightFun (implicitFunctionDataOfComplemented f f' hf hf' hker)
      (ImplicitFunctionData.pt (implicitFunctionDataOfComplemented f f' hf hf' hker)))

Tactic:
(implicitFunctionDataOfComplemented f f' hf hf' hker).hasStrictFDerivAt_implicitFunction
      f'.ker.subtypeL _ _

Premises used: Submodule.subtypeL, HasStrictFDerivAt.implicitFunctionDataOfComplemented, LinearMap.ker, ContinuousLinearMap.toLinearMap, ImplicitFunctionData.hasStrictFDerivAt_implicitFunction
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
h :
  0 =
    ImplicitFunctionData.rightFun (implicitFunctionDataOfComplemented f f' hf hf' hker)
      (ImplicitFunctionData.pt (implicitFunctionDataOfComplemented f f' hf hf' hker))
convert_1 :
  ImplicitFunctionData.rightDeriv (implicitFunctionDataOfComplemented f f' hf hf' hker) ∘SL
      (↑f' : E →ₗ[𝕜] F).ker.subtypeL =
    ContinuousLinearMap.id 𝕜 ↥(↑f' : E →ₗ[𝕜] F).ker
convert_2 :
  ImplicitFunctionData.leftDeriv (implicitFunctionDataOfComplemented f f' hf hf' hker) ∘SL
      (↑f' : E →ₗ[𝕜] F).ker.subtypeL =
    0
⊢ HasStrictFDerivAt (implicitFunctionOfComplemented f f' hf hf' hker (f a)) (↑f' : E →ₗ[𝕜] F).ker.subtypeL 0

Tactic:
convert!
    (implicitFunctionDataOfComplemented f f' hf hf' hker).hasStrictFDerivAt_implicitFunction
      f'.ker.subtypeL _ _

Premises used: Submodule.subtypeL, HasStrictFDerivAt.implicitFunctionDataOfComplemented, LinearMap.ker, ContinuousLinearMap.toLinearMap, ImplicitFunctionData.hasStrictFDerivAt_implicitFunction
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
convert_1 :
  ∀ (x : ↥(↑f' : E →ₗ[𝕜] F).ker),
    Eq.{u_2 + 1} (α := E)
      (↑((ImplicitFunctionData.rightDeriv (implicitFunctionDataOfComplemented f f' hf hf' hker) ∘SL
                (↑f' : E →ₗ[𝕜] F).ker.subtypeL :
              (a : ↥(↑f' : E →ₗ[𝕜] F).ker) → ↥(↑f' : E →ₗ[𝕜] F).ker)
            x) :
        E)
      (↑((ContinuousLinearMap.id 𝕜 ↥(↑f' : E →ₗ[𝕜] F).ker : (a : ↥(↑f' : E →ₗ[𝕜] F).ker) → ↥(↑f' : E →ₗ[𝕜] F).ker) x) :
        E)
⊢ ImplicitFunctionData.rightDeriv (implicitFunctionDataOfComplemented f f' hf hf' hker) ∘SL
      (↑f' : E →ₗ[𝕜] F).ker.subtypeL =
    ContinuousLinearMap.id 𝕜 ↥(↑f' : E →ₗ[𝕜] F).ker

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
x : ↥(↑f' : E →ₗ[𝕜] F).ker
⊢ Eq.{u_2 + 1} (α := E)
    (↑((ImplicitFunctionData.rightDeriv (implicitFunctionDataOfComplemented f f' hf hf' hker) ∘SL
              (↑f' : E →ₗ[𝕜] F).ker.subtypeL :
            (a : ↥(↑f' : E →ₗ[𝕜] F).ker) → ↥(↑f' : E →ₗ[𝕜] F).ker)
          x) :
      E)
    (↑((ContinuousLinearMap.id 𝕜 ↥(↑f' : E →ₗ[𝕜] F).ker : (a : ↥(↑f' : E →ₗ[𝕜] F).ker) → ↥(↑f' : E →ₗ[𝕜] F).ker) x) : E)

Tactic:
simp only [Classical.choose_spec hker, implicitFunctionDataOfComplemented,
      ContinuousLinearMap.comp_apply, Submodule.coe_subtypeL, Submodule.coe_subtype,
      ContinuousLinearMap.id_apply]

Premises used: HasStrictFDerivAt.implicitFunctionDataOfComplemented, ContinuousLinearMap.id_apply, Classical.choose_spec, Submodule.coe_subtype, Submodule.coe_subtypeL, ContinuousLinearMap.comp_apply
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
convert_2 :
  ∀ (x : ↥(↑f' : E →ₗ[𝕜] F).ker),
    Eq.{u_3 + 1} (α := F)
      ((ImplicitFunctionData.leftDeriv (implicitFunctionDataOfComplemented f f' hf hf' hker) ∘SL
              (↑f' : E →ₗ[𝕜] F).ker.subtypeL :
            (a : ↥(↑f' : E →ₗ[𝕜] F).ker) → F)
          x :
        F)
      ((0 : (a : ↥(↑f' : E →ₗ[𝕜] F).ker) → F) x : F)
⊢ ImplicitFunctionData.leftDeriv (implicitFunctionDataOfComplemented f f' hf hf' hker) ∘SL
      (↑f' : E →ₗ[𝕜] F).ker.subtypeL =
    0

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
x : ↥(↑f' : E →ₗ[𝕜] F).ker
⊢ Eq.{u_3 + 1} (α := F)
    ((ImplicitFunctionData.leftDeriv (implicitFunctionDataOfComplemented f f' hf hf' hker) ∘SL
            (↑f' : E →ₗ[𝕜] F).ker.subtypeL :
          (a : ↥(↑f' : E →ₗ[𝕜] F).ker) → F)
        x :
      F)
    ((0 : (a : ↥(↑f' : E →ₗ[𝕜] F).ker) → F) x : F)

Tactic:
simp only [ContinuousLinearMap.comp_apply, Submodule.coe_subtypeL, Submodule.coe_subtype,
      ContinuousLinearMap.apply_val_ker, ContinuousLinearMap.zero_apply]

Premises used: Submodule.coe_subtype, ContinuousLinearMap.apply_val_ker, Submodule.coe_subtypeL, ContinuousLinearMap.zero_apply, ContinuousLinearMap.comp_apply
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
hker : (↑f' : E →ₗ[𝕜] F).ker.ClosedComplemented
⊢ 0 =
    ImplicitFunctionData.rightFun (implicitFunctionDataOfComplemented f f' hf hf' hker)
      (ImplicitFunctionData.pt (implicitFunctionDataOfComplemented f f' hf hf' hker))

Tactic:
simp only [implicitFunctionDataOfComplemented, map_sub, sub_self]

Premises used: HasStrictFDerivAt.implicitFunctionDataOfComplemented, map_sub, sub_self
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
x : E
⊢ ((↑(implicitToOpenPartialHomeomorph f f' hf hf') : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) x).1 = f x

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
y : ↥(↑f' : E →ₗ[𝕜] F).ker
⊢ (↑(implicitToOpenPartialHomeomorph f f' hf hf') : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) ((↑y : E) + a) =
    (f ((↑y : E) + a), y)

Tactic:
have := FiniteDimensional.complete 𝕜 F
  implicitToOpenPartialHomeomorphOfComplemented_apply_ker ..

Premises used: _private.0.HasStrictFDerivAt.implicitToOpenPartialHomeomorph._proof_2, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply_ker, HasStrictFDerivAt.implicitToOpenPartialHomeomorph, FiniteDimensional.complete
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
⊢ (↑(implicitToOpenPartialHomeomorph f f' hf hf') : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) a = (f a, 0)

Tactic:
have := FiniteDimensional.complete 𝕜 F
  implicitToOpenPartialHomeomorphOfComplemented_self ..

Premises used: _private.0.HasStrictFDerivAt.implicitToOpenPartialHomeomorph._proof_2, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_self, HasStrictFDerivAt.implicitToOpenPartialHomeomorph, FiniteDimensional.complete
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
⊢ a ∈ (implicitToOpenPartialHomeomorph f f' hf hf').source

Tactic:
have := FiniteDimensional.complete 𝕜 F
  ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source _

Premises used: HasStrictFDerivAt.implicitFunctionDataOfComplemented, Set.Mem, ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source, _private.0.HasStrictFDerivAt.implicitToOpenPartialHomeomorph._proof_2, FiniteDimensional.complete
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
⊢ (f a, 0) ∈ (implicitToOpenPartialHomeomorph f f' hf hf').target

Tactic:
have := FiniteDimensional.complete 𝕜 F
  mem_implicitToOpenPartialHomeomorphOfComplemented_target ..

Premises used: Set.Mem, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_target, _private.0.HasStrictFDerivAt.implicitToOpenPartialHomeomorph._proof_2, FiniteDimensional.complete
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → ↥(↑f' : E →ₗ[𝕜] F).ker
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:
((hf.implicitToOpenPartialHomeomorph f f' hf').tendsto_symm
    (hf.mem_implicitToOpenPartialHomeomorph_source hf')).comp ?_

Premises used: HasStrictFDerivAt.implicitToOpenPartialHomeomorph, HasStrictFDerivAt.implicitFunction, Filter.Tendsto.comp, OpenPartialHomeomorph.tendsto_symm, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_source
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → ↥(↑f' : E →ₗ[𝕜] F).ker
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
refine :
  Tendsto (fun (t : α) ↦ (g₁ t, g₂ t)) l
    (𝓝 ((↑(implicitToOpenPartialHomeomorph f f' hf hf') : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) a))
⊢ Tendsto (fun (t : α) ↦ implicitFunction f f' hf hf' (g₁ t) (g₂ t)) l (𝓝 a)

Tactic:
refine ((hf.implicitToOpenPartialHomeomorph f f' hf').tendsto_symm
    (hf.mem_implicitToOpenPartialHomeomorph_source hf')).comp ?_

Premises used: HasStrictFDerivAt.implicitToOpenPartialHomeomorph, Filter.Tendsto.comp, OpenPartialHomeomorph.tendsto_symm, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_source
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → ↥(↑f' : E →ₗ[𝕜] F).ker
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
rw : Tendsto (β := Prod.{u_3, u_2} F ↥(↑f' : E →ₗ[𝕜] F).ker) (fun (t : α) ↦ (g₁ t, g₂ t)) l (𝓝 (f a, 0))
⊢ Tendsto (fun (t : α) ↦ (g₁ t, g₂ t)) l
    (𝓝 ((↑(implicitToOpenPartialHomeomorph f f' hf hf') : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) a))

Tactic:
rw [implicitToOpenPartialHomeomorph_self]

Premises used: HasStrictFDerivAt.implicitToOpenPartialHomeomorph_self
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → ↥(↑f' : E →ₗ[𝕜] F).ker
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
⊢ Tendsto (β := Prod.{u_3, u_2} F ↥(↑f' : E →ₗ[𝕜] F).ker) (fun (t : α) ↦ (g₁ t, g₂ t)) l (𝓝 (f a, 0))

Tactic:
h₁.prodMk_nhds h₂

Premises used: Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → ↥(↑f' : E →ₗ[𝕜] F).ker
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
⊢ Tendsto (β := Prod.{u_3, u_2} F ↥(↑f' : E →ₗ[𝕜] F).ker) (fun (t : α) ↦ (g₁ t, g₂ t)) l (𝓝 (f a, 0))

Tactic:
exact h₁.prodMk_nhds h₂

Premises used: Filter.Tendsto.prodMk_nhds