awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h :
  ∀ (S : L.Substructure M),
    S.FG →
      ∀ (f : Embedding.{u, v, w, w'} L (↥S) N) (m : M),
        ∃ (g : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S)) N),
          f = g.comp (Substructure.inclusion ⋯)
x : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
f' : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ f.dom)) N
eq_f' : f.toEmbedding = f'.comp (Substructure.inclusion ⋯)
⊢ ∃ (g : L.FGEquiv M N), m ∈ (↑g : M ≃ₚ[L] N).dom ∧ Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG ≤ g
have refine_2 : ∀ (x : ↥(↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).dom),
  Eq.{w' + 1} (α := N)
    (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                        { dom := LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ f.dom, cod := f'.toHom.range,
                          toEquiv := f'.equivRange : M ≃ₚ[L] N }
                        sorry) :
                    M ≃ₚ[L] N).cod.subtype.comp
            ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                          { dom := LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ f.dom, cod := f'.toHom.range,
                            toEquiv := f'.equivRange : M ≃ₚ[L] N }
                          sorry) :
                      M ≃ₚ[L] N).toEquiv.toEmbedding.comp
              (Substructure.inclusion sorry)) :
          (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] N).dom) → N)
        x :
      N)
    (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).cod.subtype.comp
            (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).toEquiv.toEmbedding :
          (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] N).dom) → N)
        x :
      N)
Tactic: refine ⟨⟨⟨closure L {m} ⊔ f.dom, f'.toHom.range, f'.equivRange⟩,
      (fg_closure_singleton _).sup f_FG⟩,
      subset_closure.trans (le_sup_left : (closure L) {m} ≤ _) (mem_singleton m),
      ⟨le_sup_right, Embedding.ext (fun _ => ?_)⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h :
  ∀ (S : L.Substructure M),
    S.FG →
      ∀ (f : Embedding.{u, v, w, w'} L (↥S) N) (m : M),
        ∃ (g : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S)) N),
          f = g.comp (Substructure.inclusion ⋯)
x : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
f' : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ f.dom)) N
eq_f' : f.toEmbedding = f'.comp (Substructure.inclusion ⋯)
x_1 : ↥(↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).dom
⊢ Eq.{w' + 1} (α := N)
    (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                        { dom := LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ f.dom, cod := f'.toHom.range,
                          toEquiv := f'.equivRange : M ≃ₚ[L] N }
                        ⋯) :
                    M ≃ₚ[L] N).cod.subtype.comp
            ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                          { dom := LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ f.dom, cod := f'.toHom.range,
                            toEquiv := f'.equivRange : M ≃ₚ[L] N }
                          ⋯) :
                      M ≃ₚ[L] N).toEquiv.toEmbedding.comp
              (Substructure.inclusion ⋯)) :
          (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] N).dom) → N)
        x_1 :
      N)
    (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).cod.subtype.comp
            (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).toEquiv.toEmbedding :
          (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] N).dom) → N)
        x_1 :
      N)
have refine_2 : ∀ (eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion sorry))
  (x : ↥(↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).dom),
  Eq.{w' + 1} (α := N)
    (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                        { dom := LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ f.dom, cod := f'.toHom.range,
                          toEquiv := f'.equivRange : M ≃ₚ[L] N }
                        sorry) :
                    M ≃ₚ[L] N).cod.subtype.comp
            ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                          { dom := LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ f.dom, cod := f'.toHom.range,
                            toEquiv := f'.equivRange : M ≃ₚ[L] N }
                          sorry) :
                      M ≃ₚ[L] N).toEquiv.toEmbedding.comp
              (Substructure.inclusion sorry)) :
          (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] N).dom) → N)
        x :
      N)
    (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).cod.subtype.comp
            (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).toEquiv.toEmbedding :
          (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] N).dom) → N)
        x :
      N)
Tactic: rw [PartialEquiv.toEmbedding] at eq_f'
Cleared hypotheses: eq_f', x_1
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
M_cg : Structure.CG L M
g : L.FGEquiv M N
H : L.IsExtensionPair M N
⊢ ∃ (f : M ↪[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toPartialEquiv
have rcases : ∀ (X : Set M),
  X.Countable →
    ∀ (X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤),
      ∃ (f : M ↪[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toPartialEquiv
Tactic: rcases M_cg with ⟨X, _, X_gen⟩
Cleared hypotheses: M_cg
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
⊢ ∃ (f : M ↪[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toPartialEquiv
have x : Countable.{w + 1} (↑X : Type w)
Tactic: have _ : Countable (↑X : Type _) := by simpa only [countable_coe_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
h : Countable.{w + 1} (↑X : Type w)
⊢ ∃ (f : M ↪[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toPartialEquiv
have have : ∀ (x : Encodable (↑X : Type w)), ∃ (f : M ↪[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toPartialEquiv
Tactic: have _ : Encodable (↑X : Type _) := Encodable.ofCountable _
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
h : Countable.{w + 1} (↑X : Type w)
x_1 : Encodable (↑X : Type w)
D : (↑X : Type w) → Order.Cofinal (L.FGEquiv M N) := fun (x : (↑X : Type w)) ↦ H.definedAtLeft (↑x : M)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x : M
hx : x ∈ X
⊢ x ∈ (↑F.dom : Set M)
have this : Order.sequenceOfCofinals g D (Encodable.encode (Subtype.mk (p := fun (x : M) ↦ x ∈ X) x hx) + 1) ∈
  D (Subtype.mk (p := fun (x : M) ↦ x ∈ X) x hx)
Tactic: have := Order.sequenceOfCofinals.encode_mem g D ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
D : (↑X : Type w) → Order.Cofinal (L.FGEquiv M N) := fun (x : (↑X : Type w)) ↦ H.definedAtLeft (↑x : M)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
⊢ ∃ (f : M ↪[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toPartialEquiv
have x : X ⊆ (↑F.dom : Set M)
Tactic: have _ : X ⊆ F.dom := by
    intro x hx
    have := Order.sequenceOfCofinals.encode_mem g D ⟨x, hx⟩
    exact dom_le_dom
      (le_partialEquivLimit S (Encodable.encode (⟨x, hx⟩ : X) + 1)) this
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
D : (↑X : Type w) → Order.Cofinal (L.FGEquiv M N) := fun (x : (↑X : Type w)) ↦ H.definedAtLeft (↑x : M)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_1 : X ⊆ (↑F.dom : Set M)
⊢ F.dom = ⊤
have rwa : ⊤ ≤ F.dom
Tactic: rwa [← top_le_iff, ← X_gen, Substructure.closure_le]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
D : (↑X : Type w) → Order.Cofinal (L.FGEquiv M N) := fun (x : (↑X : Type w)) ↦ H.definedAtLeft (↑x : M)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_1 : X ⊆ (↑F.dom : Set M)
rwa : ⊤ ≤ F.dom
⊢ F.dom = ⊤
have rwa₁ : LowerAdjoint.toFun (u := SetLike.coe) (closure L) X ≤ F.dom
Tactic: rwa [← top_le_iff, ← X_gen, Substructure.closure_le]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
D : (↑X : Type w) → Order.Cofinal (L.FGEquiv M N) := fun (x : (↑X : Type w)) ↦ H.definedAtLeft (↑x : M)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_1 : X ⊆ (↑F.dom : Set M)
⊢ ∃ (f : M ↪[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toPartialEquiv
have isTop : F.dom = ⊤
Tactic: have isTop : F.dom = ⊤ := by rwa [← top_le_iff, ← X_gen, Substructure.closure_le]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
D : (↑X : Type w) → Order.Cofinal (L.FGEquiv M N) := fun (x : (↑X : Type w)) ↦ H.definedAtLeft (↑x : M)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_1 : X ⊆ (↑F.dom : Set M)
isTop : F.dom = ⊤
⊢ (↑g : M ≃ₚ[L] N) ≤ (toEmbeddingOfEqTop isTop).toPartialEquiv
have h : (toEmbeddingOfEqTop isTop).toPartialEquiv = partialEquivLimit S
Tactic: convert! (le_partialEquivLimit S 0)
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
M_cg : Structure.CG L M
N_cg : Structure.CG L N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
have rcases : ∀ (X : Set M) (X_count : X.Countable)
  (X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤),
  ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
Tactic: rcases M_cg with ⟨X, X_count, X_gen⟩
Cleared hypotheses: M_cg
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
N_cg : Structure.CG L N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
have rcases : ∀ (Y : Set N) (Y_count : Y.Countable)
  (Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤),
  ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
Tactic: rcases N_cg with ⟨Y, Y_count, Y_gen⟩
Cleared hypotheses: N_cg
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
have x : Countable.{w + 1} (↑X : Type w)
Tactic: have _ : Countable (↑X : Type _) := by simpa only [countable_coe_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h : Countable.{w + 1} (↑X : Type w)
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
have have : ∀ (x : Encodable (↑X : Type w)), ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
Tactic: have _ : Encodable (↑X : Type _) := Encodable.ofCountable _
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
have x : Countable.{w' + 1} (↑Y : Type w')
Tactic: have _ : Countable (↑Y : Type _) := by simpa only [countable_coe_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
h_1 : Countable.{w' + 1} (↑Y : Type w')
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
have have : ∀ (x : Encodable (↑Y : Type w')), ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
Tactic: have _ : Encodable (↑Y : Type _) := Encodable.ofCountable _
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h : Countable.{w + 1} (↑X : Type w)
x_1 : Encodable (↑X : Type w)
h_1 : Countable.{w' + 1} (↑Y : Type w')
x_2 : Encodable (↑Y : Type w')
D : Sum.{w, w'} (↑X : Type w) (↑Y : Type w') → Order.Cofinal (L.FGEquiv M N) :=
  fun (p : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦
    Sum.recOn (motive := fun (x : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦ Order.Cofinal (L.FGEquiv M N)) p
      (fun (x : (↑X : Type w)) ↦ ext_dom.definedAtLeft (↑x : M)) fun (y : (↑Y : Type w')) ↦
      ext_cod.definedAtRight (↑y : N)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x : M
hx : x ∈ X
⊢ x ∈ (↑F.dom : Set M)
have this : Order.sequenceOfCofinals g D
    (Encodable.encode (α := Sum.{w, w'} (↑X : Type w) (↑Y : Type w'))
        (Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ X) x hx)) +
      1) ∈
  D (Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ X) x hx))
Tactic: have := Order.sequenceOfCofinals.encode_mem g D (Sum.inl ⟨x, hx⟩)
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
h_1 : Countable.{w' + 1} (↑Y : Type w')
x_1 : Encodable (↑Y : Type w')
D : Sum.{w, w'} (↑X : Type w) (↑Y : Type w') → Order.Cofinal (L.FGEquiv M N) :=
  fun (p : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦
    Sum.recOn (motive := fun (x : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦ Order.Cofinal (L.FGEquiv M N)) p
      (fun (x : (↑X : Type w)) ↦ ext_dom.definedAtLeft (↑x : M)) fun (y : (↑Y : Type w')) ↦
      ext_cod.definedAtRight (↑y : N)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
have x : X ⊆ (↑F.dom : Set M)
Tactic: have _ : X ⊆ F.dom := by
    intro x hx
    have := Order.sequenceOfCofinals.encode_mem g D (Sum.inl ⟨x, hx⟩)
    exact dom_le_dom
      (le_partialEquivLimit S (Encodable.encode (Sum.inl (⟨x, hx⟩ : X)) + 1)) this
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
h_1 : Countable.{w' + 1} (↑Y : Type w')
x_1 : Encodable (↑Y : Type w')
D : Sum.{w, w'} (↑X : Type w) (↑Y : Type w') → Order.Cofinal (L.FGEquiv M N) :=
  fun (p : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦
    Sum.recOn (motive := fun (x : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦ Order.Cofinal (L.FGEquiv M N)) p
      (fun (x : (↑X : Type w)) ↦ ext_dom.definedAtLeft (↑x : M)) fun (y : (↑Y : Type w')) ↦
      ext_cod.definedAtRight (↑y : N)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_2 : X ⊆ (↑F.dom : Set M)
y : N
hy : y ∈ Y
⊢ y ∈ (↑F.cod : Set N)
have this : Order.sequenceOfCofinals g D
    (Encodable.encode (α := Sum.{w, w'} (↑X : Type w) (↑Y : Type w'))
        (Sum.inr (Subtype.mk (p := fun (x : N) ↦ x ∈ Y) y hy)) +
      1) ∈
  D (Sum.inr (Subtype.mk (p := fun (x : N) ↦ x ∈ Y) y hy))
Tactic: have := Order.sequenceOfCofinals.encode_mem g D (Sum.inr ⟨y, hy⟩)
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
h_1 : Countable.{w' + 1} (↑Y : Type w')
x_1 : Encodable (↑Y : Type w')
D : Sum.{w, w'} (↑X : Type w) (↑Y : Type w') → Order.Cofinal (L.FGEquiv M N) :=
  fun (p : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦
    Sum.recOn (motive := fun (x : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦ Order.Cofinal (L.FGEquiv M N)) p
      (fun (x : (↑X : Type w)) ↦ ext_dom.definedAtLeft (↑x : M)) fun (y : (↑Y : Type w')) ↦
      ext_cod.definedAtRight (↑y : N)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_2 : X ⊆ (↑F.dom : Set M)
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
have x : Y ⊆ (↑F.cod : Set N)
Tactic: have _ : Y ⊆ F.cod := by
    intro y hy
    have := Order.sequenceOfCofinals.encode_mem g D (Sum.inr ⟨y, hy⟩)
    exact cod_le_cod
      (le_partialEquivLimit S (Encodable.encode (Sum.inr (⟨y, hy⟩ : Y)) + 1)) this
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
h_1 : Countable.{w' + 1} (↑Y : Type w')
x_1 : Encodable (↑Y : Type w')
D : Sum.{w, w'} (↑X : Type w) (↑Y : Type w') → Order.Cofinal (L.FGEquiv M N) :=
  fun (p : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦
    Sum.recOn (motive := fun (x : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦ Order.Cofinal (L.FGEquiv M N)) p
      (fun (x : (↑X : Type w)) ↦ ext_dom.definedAtLeft (↑x : M)) fun (y : (↑Y : Type w')) ↦
      ext_cod.definedAtRight (↑y : N)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_2 : X ⊆ (↑F.dom : Set M)
h_3 : Y ⊆ (↑F.cod : Set N)
⊢ F.dom = ⊤
have rwa : ⊤ ≤ F.dom
Tactic: rwa [← top_le_iff, ← X_gen, Substructure.closure_le]