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
x : G
y : E
simp :
  (fderiv 𝕜
            (fun (b : G) ↦
              HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯)
                φ.pt ⋯ (φ.leftFun φ.pt, b))
            (φ.rightFun φ.pt) :
          (a : G) → E)
        x =
      y ↔
    Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) y : F) (0 : F) ∧ (φ.rightDeriv : (a : E) → G) y = x
⊢ (fderiv 𝕜
            (fun (b : G) ↦
              (↑(HasStrictFDerivAt.toOpenPartialHomeomorph φ.prodFun ⋯).symm : F × G → E) (φ.leftFun φ.pt, b))
            (φ.rightFun φ.pt) :
          (a : G) → E)
        x =
      y ↔
    Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) y : F) (0 : F) ∧ (φ.rightDeriv : (a : E) → G) y = x

Tactic:
simp only [← HasStrictFDerivAt.localInverse_def]

Premises used: HasStrictFDerivAt.localInverse_def
-- 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
x : G
y : E
rw :
  ((↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm : F × G →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
            (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G)) :
          (a : G) → E)
        x =
      y ↔
    Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) y : F) (0 : F) ∧ (φ.rightDeriv : (a : E) → G) y = x
⊢ (fderiv 𝕜
            (fun (b : G) ↦
              HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯)
                φ.pt ⋯ (φ.leftFun φ.pt, b))
            (φ.rightFun φ.pt) :
          (a : G) → E)
        x =
      y ↔
    Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) y : F) (0 : F) ∧ (φ.rightDeriv : (a : E) → G) y = x

Tactic:
rw [φ.hasStrictFDerivAt.to_localInverse.comp (φ.rightFun φ.pt)
    ((hasStrictFDerivAt_const _ _).prodMk (hasStrictFDerivAt_id _)) |>.hasFDerivAt |>.fderiv]

Premises used: ImplicitFunctionData.pt, HasStrictFDerivAt.prodMk, ImplicitFunctionData.hasStrictFDerivAt, HasStrictFDerivAt.hasFDerivAt, HasFDerivAt.fderiv, HasStrictFDerivAt.to_localInverse, HasStrictFDerivAt.comp, hasStrictFDerivAt_const, ImplicitFunctionData.rightFun, hasStrictFDerivAt_id
-- 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
x : G
y : E
⊢ ((↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm : F × G →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
            (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G)) :
          (a : G) → E)
        x =
      y ↔
    Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) y : F) (0 : F) ∧ (φ.rightDeriv : (a : E) → G) y = x

Tactic:
simp [ContinuousLinearEquiv.symm_apply_eq, @eq_comm _ (φ.leftDeriv _),
    @eq_comm _ (φ.rightDeriv _)]

Premises used: eq_comm, ContinuousLinearEquiv.symm_apply_eq
-- 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
x : G
⊢ Eq.{u_3 + 1} (α := F)
    ((φ.leftDeriv : (a : E) → F)
        ((fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) : (a : G) → E) x : E) :
      F)
    (0 : F)

Tactic:
φ.fderiv_implicitFunction_apply_eq_iff.mp rfl |>.left

Premises used: ImplicitFunctionData.fderiv_implicitFunction_apply_eq_iff, And.left, Iff.mp, 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
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
x : G
⊢ Eq.{u_3 + 1} (α := F)
    ((φ.leftDeriv : (a : E) → F)
        ((fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) : (a : G) → E) x : E) :
      F)
    (0 : F)

Tactic:
exact φ.fderiv_implicitFunction_apply_eq_iff.mp rfl |>.left

Premises used: ImplicitFunctionData.fderiv_implicitFunction_apply_eq_iff, And.left, Iff.mp, 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
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
x : G
⊢ (φ.rightDeriv : (a : E) → G)
      ((fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) : (a : G) → E) x : E) =
    x

Tactic:
φ.fderiv_implicitFunction_apply_eq_iff.mp rfl |>.right

Premises used: ImplicitFunctionData.fderiv_implicitFunction_apply_eq_iff, And.right, Iff.mp, 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
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
x : G
⊢ (φ.rightDeriv : (a : E) → G)
      ((fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) : (a : G) → E) x : E) =
    x

Tactic:
exact φ.fderiv_implicitFunction_apply_eq_iff.mp rfl |>.right

Premises used: ImplicitFunctionData.fderiv_implicitFunction_apply_eq_iff, And.right, Iff.mp, 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
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
g'inv : G →L[𝕜] E
hg'inv : φ.rightDeriv ∘SL g'inv = ContinuousLinearMap.id 𝕜 G
hg'invf : φ.leftDeriv ∘SL g'inv = 0
⊢ HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt))
    (fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)) (φ.rightFun φ.pt)

Tactic:
φ.hasStrictFDerivAt_implicitFunction_fderiv

Premises used: ImplicitFunctionData.hasStrictFDerivAt_implicitFunction_fderiv
-- 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
g'inv : G →L[𝕜] E
hg'inv : φ.rightDeriv ∘SL g'inv = ContinuousLinearMap.id 𝕜 G
hg'invf : φ.leftDeriv ∘SL g'inv = 0
h : g'inv = fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)
⊢ HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt)) g'inv (φ.rightFun φ.pt)

Tactic:
convert! φ.hasStrictFDerivAt_implicitFunction_fderiv

Premises used: ImplicitFunctionData.hasStrictFDerivAt_implicitFunction_fderiv
-- 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
g'inv : G →L[𝕜] E
hg'inv : φ.rightDeriv ∘SL g'inv = ContinuousLinearMap.id 𝕜 G
hg'invf : φ.leftDeriv ∘SL g'inv = 0
h :
  ∀ (x : G),
    Eq.{u_2 + 1} (α := E) ((g'inv : (a : G) → E) x : E)
      ((fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) : (a : G) → E) x : E)
⊢ g'inv = fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)

Tactic:
ext1 x
-- 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
g'inv : G →L[𝕜] E
hg'inv : φ.rightDeriv ∘SL g'inv = ContinuousLinearMap.id 𝕜 G
hg'invf : φ.leftDeriv ∘SL g'inv = 0
x : G
h :
  Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) ((g'inv : (a : G) → E) x : E) : F) (0 : F) ∧
    (φ.rightDeriv : (a : E) → G) ((g'inv : (a : G) → E) x : E) = x
⊢ Eq.{u_2 + 1} (α := E) ((g'inv : (a : G) → E) x : E)
    ((fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) : (a : G) → E) x : E)

Tactic:
rw [eq_comm, fderiv_implicitFunction_apply_eq_iff]

Premises used: eq_comm, ImplicitFunctionData.fderiv_implicitFunction_apply_eq_iff
-- 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
g'inv : G →L[𝕜] E
hg'inv : φ.rightDeriv ∘SL g'inv = ContinuousLinearMap.id 𝕜 G
hg'invf : φ.leftDeriv ∘SL g'inv = 0
x : G
⊢ Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) ((g'inv : (a : G) → E) x : E) : F) (0 : F) ∧
    (φ.rightDeriv : (a : E) → G) ((g'inv : (a : G) → E) x : E) = x

Tactic:
simp_all [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- 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
s : Set E
⊢ φ.implicitFunction (φ.leftFun φ.pt) =
    (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)

Tactic:
have H : φ.implicitFunction (φ.leftFun φ.pt) =
      φ.toOpenPartialHomeomorph.symm ∘ (φ.leftFun φ.pt, ·) := 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
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
s : Set E
H :
  φ.implicitFunction (φ.leftFun φ.pt) =
    (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)
rw :
  𝓝[φ.toOpenPartialHomeomorph.symm.target ∩
        (↑φ.toOpenPartialHomeomorph.symm.symm : E → F × G) ⁻¹'
          SProd.sprod (α := Set F) (β := Set G) {φ.leftFun φ.pt}
            (((↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)) ⁻¹' s)]
      φ.pt =
    𝓝[s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt}] φ.pt
hx : (φ.leftFun φ.pt, φ.rightFun φ.pt) ∈ φ.toOpenPartialHomeomorph.symm.source
⊢ map (φ.implicitFunction (φ.leftFun φ.pt)) (𝓝[φ.implicitFunction (φ.leftFun φ.pt) ⁻¹' s] φ.rightFun φ.pt) =
    𝓝[s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt}] φ.pt

Tactic:
rw [H, ← Filter.map_map, (isInducing_prodMkRight _).map_nhdsWithin_eq, ← Set.singleton_prod,
    OpenPartialHomeomorph.map_nhdsWithin_eq, ← prodFun_apply, ← toOpenPartialHomeomorph_coe,
    φ.toOpenPartialHomeomorph.leftInvOn φ.pt_mem_toOpenPartialHomeomorph_source,
    OpenPartialHomeomorph.image_source_inter_eq']

Premises used: Topology.IsInducing.map_nhdsWithin_eq, OpenPartialHomeomorph.map_nhdsWithin_eq, ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source, OpenPartialHomeomorph.leftInvOn, Filter.map_map, Set.singleton_prod, ImplicitFunctionData.prodFun_apply, ImplicitFunctionData.toOpenPartialHomeomorph, OpenPartialHomeomorph.image_source_inter_eq', isInducing_prodMkRight, ImplicitFunctionData.toOpenPartialHomeomorph_coe
-- 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
s : Set E
H :
  φ.implicitFunction (φ.leftFun φ.pt) =
    (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)
rw : 𝓝[φ.toOpenPartialHomeomorph.source ∩ (s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt})] φ.pt
| 𝓝[s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt}] φ.pt

Tactic:
rw [← φ.toOpenPartialHomeomorph.nhdsWithin_source_inter
        φ.pt_mem_toOpenPartialHomeomorph_source]

Premises used: ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source, ImplicitFunctionData.toOpenPartialHomeomorph, OpenPartialHomeomorph.nhdsWithin_source_inter
-- 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
s : Set E
H :
  φ.implicitFunction (φ.leftFun φ.pt) =
    (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)
conv_rhs :
  𝓝[φ.toOpenPartialHomeomorph.symm.target ∩
        (↑φ.toOpenPartialHomeomorph.symm.symm : E → F × G) ⁻¹'
          SProd.sprod (α := Set F) (β := Set G) {φ.leftFun φ.pt}
            (((↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)) ⁻¹' s)]
      φ.pt =
    𝓝[φ.toOpenPartialHomeomorph.source ∩ (s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt})] φ.pt
⊢ 𝓝[φ.toOpenPartialHomeomorph.symm.target ∩
        (↑φ.toOpenPartialHomeomorph.symm.symm : E → F × G) ⁻¹'
          SProd.sprod (α := Set F) (β := Set G) {φ.leftFun φ.pt}
            (((↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)) ⁻¹' s)]
      φ.pt =
    𝓝[s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt}] φ.pt

Tactic:
conv_rhs =>
      rw [← φ.toOpenPartialHomeomorph.nhdsWithin_source_inter
        φ.pt_mem_toOpenPartialHomeomorph_source]

Premises used: ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source, ImplicitFunctionData.toOpenPartialHomeomorph, OpenPartialHomeomorph.nhdsWithin_source_inter
-- 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
s : Set E
H :
  φ.implicitFunction (φ.leftFun φ.pt) =
    (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)
e_s :
  φ.toOpenPartialHomeomorph.symm.target ∩
      (↑φ.toOpenPartialHomeomorph.symm.symm : E → F × G) ⁻¹'
        SProd.sprod (α := Set F) (β := Set G) {φ.leftFun φ.pt}
          (((↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)) ⁻¹' s) =
    φ.toOpenPartialHomeomorph.source ∩ (s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt})
⊢ 𝓝[φ.toOpenPartialHomeomorph.symm.target ∩
        (↑φ.toOpenPartialHomeomorph.symm.symm : E → F × G) ⁻¹'
          SProd.sprod (α := Set F) (β := Set G) {φ.leftFun φ.pt}
            (((↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)) ⁻¹' s)]
      φ.pt =
    𝓝[φ.toOpenPartialHomeomorph.source ∩ (s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt})] φ.pt

Tactic:
congr 1
-- 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
s : Set E
H :
  φ.implicitFunction (φ.leftFun φ.pt) =
    (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)
e_s :
  ∀ (x : E),
    x ∈
        φ.toOpenPartialHomeomorph.symm.target ∩
          (↑φ.toOpenPartialHomeomorph.symm.symm : E → F × G) ⁻¹'
            SProd.sprod (α := Set F) (β := Set G) {φ.leftFun φ.pt}
              (((↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)) ⁻¹' s) ↔
      x ∈ φ.toOpenPartialHomeomorph.source ∩ (s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt})
⊢ φ.toOpenPartialHomeomorph.symm.target ∩
      (↑φ.toOpenPartialHomeomorph.symm.symm : E → F × G) ⁻¹'
        SProd.sprod (α := Set F) (β := Set G) {φ.leftFun φ.pt}
          (((↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)) ⁻¹' s) =
    φ.toOpenPartialHomeomorph.source ∩ (s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt})

Tactic:
ext x
-- 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
s : Set E
H :
  φ.implicitFunction (φ.leftFun φ.pt) =
    (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)
x : E
this :
  x ∈ φ.toOpenPartialHomeomorph.source →
    φ.leftFun x = φ.leftFun φ.pt →
      ((↑φ.toOpenPartialHomeomorph.symm : F × G → E) (φ.leftFun φ.pt, φ.rightFun x) ∈ s ↔ x ∈ s)
⊢ x ∈
      φ.toOpenPartialHomeomorph.symm.target ∩
        (↑φ.toOpenPartialHomeomorph.symm.symm : E → F × G) ⁻¹'
          SProd.sprod (α := Set F) (β := Set G) {φ.leftFun φ.pt}
            (((↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)) ⁻¹' s) ↔
    x ∈ φ.toOpenPartialHomeomorph.source ∩ (s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt})

Tactic:
simpa [@and_comm (_ = _)]

Premises used: and_comm
-- 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
s : Set E
H :
  φ.implicitFunction (φ.leftFun φ.pt) =
    (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)
x : E
e_s :
  x ∈ φ.toOpenPartialHomeomorph.source →
    φ.leftFun x = φ.leftFun φ.pt →
      ((↑φ.toOpenPartialHomeomorph.symm : F × G → E) (φ.leftFun φ.pt, φ.rightFun x) ∈ s ↔ x ∈ s)
⊢ x ∈
      φ.toOpenPartialHomeomorph.symm.target ∩
        (↑φ.toOpenPartialHomeomorph.symm.symm : E → F × G) ⁻¹'
          SProd.sprod (α := Set F) (β := Set G) {φ.leftFun φ.pt}
            (((↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)) ⁻¹' s) ↔
    x ∈ φ.toOpenPartialHomeomorph.source ∩ (s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt})

Tactic:
suffices x ∈ φ.toOpenPartialHomeomorph.source → φ.leftFun x = φ.leftFun φ.pt →
        (φ.toOpenPartialHomeomorph.symm (φ.leftFun φ.pt, φ.rightFun x) ∈ s ↔ x ∈ s) by
      simpa [@and_comm (_ = _)]
-- 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
s : Set E
H :
  φ.implicitFunction (φ.leftFun φ.pt) =
    (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)
x : E
hxs : x ∈ φ.toOpenPartialHomeomorph.source
hx_eq : φ.leftFun x = φ.leftFun φ.pt
e_s : (↑φ.toOpenPartialHomeomorph.symm : F × G → E) (φ.leftFun x, φ.rightFun x) ∈ s ↔ x ∈ s
e_s₁ : (↑φ.toOpenPartialHomeomorph.symm : F × G → E) (φ.prodFun x) ∈ s ↔ x ∈ s
e_s₂ : (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ((↑φ.toOpenPartialHomeomorph : E → F × G) x) ∈ s ↔ x ∈ s
e_s₃ e_s₄ : x ∈ s ↔ x ∈ s
⊢ (↑φ.toOpenPartialHomeomorph.symm : F × G → E) (φ.leftFun φ.pt, φ.rightFun x) ∈ s ↔ x ∈ s

Tactic:
rw [← hx_eq, ← prodFun_apply, ← toOpenPartialHomeomorph_coe,
      φ.toOpenPartialHomeomorph.leftInvOn hxs]

Premises used: OpenPartialHomeomorph.leftInvOn, ImplicitFunctionData.prodFun_apply, ImplicitFunctionData.toOpenPartialHomeomorph, ImplicitFunctionData.toOpenPartialHomeomorph_coe
-- 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
s : Set E
H :
  φ.implicitFunction (φ.leftFun φ.pt) =
    (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)
⊢ (φ.leftFun φ.pt, φ.rightFun φ.pt) ∈ φ.toOpenPartialHomeomorph.symm.source

Tactic:
φ.toOpenPartialHomeomorph.mapsTo φ.pt_mem_toOpenPartialHomeomorph_source

Premises used: Set.Mem, ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source, setOf, OpenPartialHomeomorph.toFun', ImplicitFunctionData.toOpenPartialHomeomorph, Set.image, OpenPartialHomeomorph.mapsTo, ImplicitFunctionData.prodFun
-- 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
s : Set E
H :
  φ.implicitFunction (φ.leftFun φ.pt) =
    (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ∘ fun (x : G) ↦ (φ.leftFun φ.pt, x)
⊢ (φ.leftFun φ.pt, φ.rightFun φ.pt) ∈ φ.toOpenPartialHomeomorph.symm.source

Tactic:
exact φ.toOpenPartialHomeomorph.mapsTo φ.pt_mem_toOpenPartialHomeomorph_source

Premises used: ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source, ImplicitFunctionData.toOpenPartialHomeomorph, OpenPartialHomeomorph.mapsTo