awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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_2 + 1} (α := E) ((g'inv : (a : G) → E) x : E)
    ((fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) : (a : G) → E) x : E)
have 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
Tactic: rw [eq_comm, fderiv_implicitFunction_apply_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (hypothesis)
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
⊢ map (φ.implicitFunction (φ.leftFun φ.pt)) (𝓝[φ.implicitFunction (φ.leftFun φ.pt) ⁻¹' s] φ.rightFun φ.pt) =
    𝓝[s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt}] φ.pt
have H : φ.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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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)
⊢ map (φ.implicitFunction (φ.leftFun φ.pt)) (𝓝[φ.implicitFunction (φ.leftFun φ.pt) ⁻¹' s] φ.rightFun φ.pt) =
    𝓝[s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt}] φ.pt
have 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
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']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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
⊢ map (φ.implicitFunction (φ.leftFun φ.pt)) (𝓝[φ.implicitFunction (φ.leftFun φ.pt) ⁻¹' s] φ.rightFun φ.pt) =
    𝓝[s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt}] φ.pt
have hx : (φ.leftFun φ.pt, φ.rightFun φ.pt) ∈ φ.toOpenPartialHomeomorph.symm.source
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']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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)
| 𝓝[s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt}] φ.pt
have rw : 𝓝[φ.toOpenPartialHomeomorph.source ∩ (s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt})] φ.pt
Tactic: rw [← φ.toOpenPartialHomeomorph.nhdsWithin_source_inter
        φ.pt_mem_toOpenPartialHomeomorph_source]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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)
⊢ 𝓝[φ.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
have 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
Tactic: conv_rhs =>
      rw [← φ.toOpenPartialHomeomorph.nhdsWithin_source_inter
        φ.pt_mem_toOpenPartialHomeomorph_source]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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)
⊢ 𝓝[φ.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
have 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})
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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)
⊢ φ.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})
have 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})
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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
⊢ 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})
have e_s : x ∈ φ.toOpenPartialHomeomorph.source →
  φ.leftFun x = φ.leftFun φ.pt →
    ((↑φ.toOpenPartialHomeomorph.symm : F × G → E) (φ.leftFun φ.pt, φ.rightFun x) ∈ s ↔ x ∈ s)
Tactic: suffices x ∈ φ.toOpenPartialHomeomorph.source → φ.leftFun x = φ.leftFun φ.pt →
        (φ.toOpenPartialHomeomorph.symm (φ.leftFun φ.pt, φ.rightFun x) ∈ s ↔ x ∈ s) by
      simpa [@and_comm (_ = _)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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
⊢ (↑φ.toOpenPartialHomeomorph.symm : F × G → E) (φ.leftFun φ.pt, φ.rightFun x) ∈ s ↔ x ∈ s
have e_s : (↑φ.toOpenPartialHomeomorph.symm : F × G → E) (φ.leftFun x, φ.rightFun x) ∈ s ↔ x ∈ s
Tactic: rw [← hx_eq, ← prodFun_apply, ← toOpenPartialHomeomorph_coe,
      φ.toOpenPartialHomeomorph.leftInvOn hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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
⊢ (↑φ.toOpenPartialHomeomorph.symm : F × G → E) (φ.leftFun φ.pt, φ.rightFun x) ∈ s ↔ x ∈ s
have e_s₁ : (↑φ.toOpenPartialHomeomorph.symm : F × G → E) (φ.prodFun x) ∈ s ↔ x ∈ s
Tactic: rw [← hx_eq, ← prodFun_apply, ← toOpenPartialHomeomorph_coe,
      φ.toOpenPartialHomeomorph.leftInvOn hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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
⊢ (↑φ.toOpenPartialHomeomorph.symm : F × G → E) (φ.leftFun φ.pt, φ.rightFun x) ∈ s ↔ x ∈ s
have e_s₂ : (↑φ.toOpenPartialHomeomorph.symm : F × G → E) ((↑φ.toOpenPartialHomeomorph : E → F × G) x) ∈ s ↔ x ∈ s
Tactic: rw [← hx_eq, ← prodFun_apply, ← toOpenPartialHomeomorph_coe,
      φ.toOpenPartialHomeomorph.leftInvOn hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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
⊢ (↑φ.toOpenPartialHomeomorph.symm : F × G → E) (φ.leftFun φ.pt, φ.rightFun x) ∈ s ↔ x ∈ s
have e_s₃ : x ∈ s ↔ x ∈ s
Tactic: rw [← hx_eq, ← prodFun_apply, ← toOpenPartialHomeomorph_coe,
      φ.toOpenPartialHomeomorph.leftInvOn hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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 (implicitFunctionOfComplemented f f' hf hf' hker (f a)) (↑f' : E →ₗ[𝕜] F).ker.subtypeL 0
have h : 0 =
  ImplicitFunctionData.rightFun (implicitFunctionDataOfComplemented f f' hf hf' hker)
    (ImplicitFunctionData.pt (implicitFunctionDataOfComplemented f f' hf hf' hker))
Tactic: convert!
    (implicitFunctionDataOfComplemented f f' hf hf' hker).hasStrictFDerivAt_implicitFunction
      f'.ker.subtypeL _ _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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))
⊢ HasStrictFDerivAt (implicitFunctionOfComplemented f f' hf hf' hker (f a)) (↑f' : E →ₗ[𝕜] F).ker.subtypeL 0
have convert_1 : ImplicitFunctionData.rightDeriv (implicitFunctionDataOfComplemented f f' hf hf' hker) ∘SL
    (↑f' : E →ₗ[𝕜] F).ker.subtypeL =
  ContinuousLinearMap.id 𝕜 ↥(↑f' : E →ₗ[𝕜] F).ker
Tactic: convert!
    (implicitFunctionDataOfComplemented f f' hf hf' hker).hasStrictFDerivAt_implicitFunction
      f'.ker.subtypeL _ _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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
⊢ HasStrictFDerivAt (implicitFunctionOfComplemented f f' hf hf' hker (f a)) (↑f' : E →ₗ[𝕜] F).ker.subtypeL 0
have convert_2 : ImplicitFunctionData.leftDeriv (implicitFunctionDataOfComplemented f f' hf hf' hker) ∘SL
    (↑f' : E →ₗ[𝕜] F).ker.subtypeL =
  0
Tactic: convert!
    (implicitFunctionDataOfComplemented f f' hf hf' hker).hasStrictFDerivAt_implicitFunction
      f'.ker.subtypeL _ _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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
⊢ ImplicitFunctionData.rightDeriv (implicitFunctionDataOfComplemented f f' hf hf' hker) ∘SL
      (↑f' : E →ₗ[𝕜] F).ker.subtypeL =
    ContinuousLinearMap.id 𝕜 ↥(↑f' : E →ₗ[𝕜] F).ker
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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
⊢ ImplicitFunctionData.leftDeriv (implicitFunctionDataOfComplemented f f' hf hf' hker) ∘SL
      (↑f' : E →ₗ[𝕜] F).ker.subtypeL =
    0
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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)
have refine : Tendsto (fun (t : α) ↦ (g₁ t, g₂ t)) l
  (𝓝 ((↑(implicitToOpenPartialHomeomorph f f' hf hf') : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) a))
Tactic: refine ((hf.implicitToOpenPartialHomeomorph f f' hf').tendsto_symm
    (hf.mem_implicitToOpenPartialHomeomorph_source hf')).comp ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
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 : α) ↦ (g₁ t, g₂ t)) l
    (𝓝 ((↑(implicitToOpenPartialHomeomorph f f' hf hf') : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) a))
have rw : Tendsto (β := Prod.{u_3, u_2} F ↥(↑f' : E →ₗ[𝕜] F).ker) (fun (t : α) ↦ (g₁ t, g₂ t)) l (𝓝 (f a, 0))
Tactic: rw [implicitToOpenPartialHomeomorph_self]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (hypothesis)
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 = ⊤
⊢ implicitFunction f f' hf hf' (f a) 0 = a
have this : CompleteSpace F
Tactic: have := FiniteDimensional.complete 𝕜 F
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitContDiff (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
φ : ImplicitFunctionData 𝕜 E₁ E₂ F
n : ℕ∞ω
hl : ContDiffAt 𝕜 n φ.leftFun φ.pt
hr : ContDiffAt 𝕜 n φ.rightFun φ.pt
pn : n ≠ 0
⊢ ContDiffAt 𝕜 n (Function.uncurry φ.implicitFunction) (φ.prodFun φ.pt)
have rw : ContDiffAt 𝕜 n
  (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv sorry sorry sorry) φ.pt sorry)
  (φ.prodFun φ.pt)
Tactic: rw [implicitFunction_def, Function.uncurry_curry, ← HasStrictFDerivAt.localInverse_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitContDiff (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
φ : ImplicitFunctionData 𝕜 E₁ E₂ F
n : ℕ∞ω
hl : ContDiffAt 𝕜 n φ.leftFun φ.pt
hr : ContDiffAt 𝕜 n φ.rightFun φ.pt
pn : n ≠ 0
⊢ ContDiffAt 𝕜 n
    (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯)
    (φ.prodFun φ.pt)
have refine : ContDiffAt 𝕜 n φ.prodFun φ.pt
Tactic: refine ContDiffAt.to_localInverse ?_ (φ.hasStrictFDerivAt.hasFDerivAt) pn