awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.PartialEquiv
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 = ⊤
⊢ ∃ (f : M ↪[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toPartialEquiv

Tactic:
exact ⟨toEmbeddingOfEqTop isTop,
        by convert! (le_partialEquivLimit S 0); apply Embedding.toPartialEquiv_toEmbedding⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
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
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
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv

Tactic:
rcases M_cg with ⟨X, X_count, X_gen⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
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) ⊤
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
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv

Tactic:
rcases N_cg with ⟨Y, Y_count, Y_gen⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
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) ⊤
⊢ Countable.{w + 1} (↑X : Type w)

Tactic:
simpa only [countable_coe_iff]

Premises used: Set.countable_coe_iff
-- Module: Mathlib.ModelTheory.PartialEquiv
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) ⊤
⊢ Countable.{w + 1} (↑X : Type w)

Tactic:
have _ : Countable (↑X : Type _) := by simpa only [countable_coe_iff]
-- Module: Mathlib.ModelTheory.PartialEquiv
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)
have : ∀ (x : Encodable (↑X : Type w)), ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv

Tactic:
have _ : Encodable (↑X : Type _) := Encodable.ofCountable _
-- Module: Mathlib.ModelTheory.PartialEquiv
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)
⊢ Countable.{w' + 1} (↑Y : Type w')

Tactic:
simpa only [countable_coe_iff]

Premises used: Set.countable_coe_iff
-- Module: Mathlib.ModelTheory.PartialEquiv
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)
⊢ Countable.{w' + 1} (↑Y : Type w')

Tactic:
have _ : Countable (↑Y : Type _) := by simpa only [countable_coe_iff]
-- Module: Mathlib.ModelTheory.PartialEquiv
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')
have : ∀ (x : Encodable (↑Y : Type w')), ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv

Tactic:
have _ : Encodable (↑Y : Type _) := Encodable.ofCountable _
-- Module: Mathlib.ModelTheory.PartialEquiv
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
⊢ 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⟩)
-- Module: Mathlib.ModelTheory.PartialEquiv
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
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))
⊢ x ∈ (↑F.dom : Set M)

Tactic:
dom_le_dom
      (le_partialEquivLimit S (Encodable.encode (Sum.inl (⟨x, hx⟩ : X)) + 1)) this

Premises used: FirstOrder.Language.PartialEquiv.dom_le_dom, Set.Mem, Sum.inl, Subtype.mk, HAdd.hAdd, Encodable.encode, OfNat.ofNat, FirstOrder.Language.DirectLimit.le_partialEquivLimit
-- Module: Mathlib.ModelTheory.PartialEquiv
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
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))
⊢ x ∈ (↑F.dom : Set M)

Tactic:
exact dom_le_dom
      (le_partialEquivLimit S (Encodable.encode (Sum.inl (⟨x, hx⟩ : X)) + 1)) this

Premises used: FirstOrder.Language.PartialEquiv.dom_le_dom, Sum.inl, Subtype.mk, HAdd.hAdd, Encodable.encode, OfNat.ofNat, FirstOrder.Language.DirectLimit.le_partialEquivLimit
-- Module: Mathlib.ModelTheory.PartialEquiv
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
⊢ 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
-- Module: Mathlib.ModelTheory.PartialEquiv
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
⊢ 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⟩)
-- Module: Mathlib.ModelTheory.PartialEquiv
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
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))
⊢ y ∈ (↑F.cod : Set N)

Tactic:
cod_le_cod
      (le_partialEquivLimit S (Encodable.encode (Sum.inr (⟨y, hy⟩ : Y)) + 1)) this

Premises used: Set.Mem, Subtype.mk, HAdd.hAdd, Sum.inr, FirstOrder.Language.PartialEquiv.cod_le_cod, Encodable.encode, OfNat.ofNat, FirstOrder.Language.DirectLimit.le_partialEquivLimit
-- Module: Mathlib.ModelTheory.PartialEquiv
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
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))
⊢ y ∈ (↑F.cod : Set N)

Tactic:
exact cod_le_cod
      (le_partialEquivLimit S (Encodable.encode (Sum.inr (⟨y, hy⟩ : Y)) + 1)) this

Premises used: Subtype.mk, HAdd.hAdd, Sum.inr, FirstOrder.Language.PartialEquiv.cod_le_cod, Encodable.encode, OfNat.ofNat, FirstOrder.Language.DirectLimit.le_partialEquivLimit
-- Module: Mathlib.ModelTheory.PartialEquiv
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 ⊆ (↑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
-- Module: Mathlib.ModelTheory.PartialEquiv
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)
rwa : ⊤ ≤ F.dom
rwa₁ : LowerAdjoint.toFun (u := SetLike.coe) (closure L) X ≤ F.dom
rwa₂ rwa₃ rwa₄ rwa₅ : X ⊆ (↑F.dom : Set M)
⊢ F.dom = ⊤

Tactic:
rwa [← top_le_iff, ← X_gen, Substructure.closure_le]

Premises used: top_le_iff, FirstOrder.Language.Substructure.closure_le
-- Module: Mathlib.ModelTheory.PartialEquiv
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 = ⊤

Tactic:
have dom_top : F.dom = ⊤ := by rwa [← top_le_iff, ← X_gen, Substructure.closure_le]
-- Module: Mathlib.ModelTheory.PartialEquiv
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)
dom_top : F.dom = ⊤
rwa : ⊤ ≤ F.cod
rwa₁ : LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y ≤ F.cod
rwa₂ rwa₃ rwa₄ rwa₅ : Y ⊆ (↑F.cod : Set N)
⊢ F.cod = ⊤

Tactic:
rwa [← top_le_iff, ← Y_gen, Substructure.closure_le]

Premises used: top_le_iff, FirstOrder.Language.Substructure.closure_le
-- Module: Mathlib.ModelTheory.PartialEquiv
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)
dom_top : F.dom = ⊤
⊢ F.cod = ⊤

Tactic:
have cod_top : F.cod = ⊤ := by rwa [← top_le_iff, ← Y_gen, Substructure.closure_le]