-- Mathlib/ModelTheory/PartialEquiv.lean
theorem equiv_between_cg (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 ≤ f.toEmbedding.toPartialEquiv

Proof state:
case mk.intro.intro.mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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 : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝³ : Countable ↑X
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p => Sum.recOn p (fun x => ext_dom.definedAtLeft ↑x) fun y => ext_cod.definedAtRight ↑y
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
let S : ℕ →o M ≃ₚ[L] N :=
  ⟨Subtype.val ∘ (Order.sequenceOfCofinals g D),
    (Subtype.mono_coe _).comp (Order.sequenceOfCofinals.monotone _ _)⟩

Result:
case mk.intro.intro.mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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 : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝³ : Countable ↑X
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p => Sum.recOn p (fun x => ext_dom.definedAtLeft ↑x) fun y => ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Proof state:
case mk.intro.intro.mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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 : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝³ : Countable ↑X
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
let D : Sum X Y → Order.Cofinal (FGEquiv L M N) := fun p ↦
  Sum.recOn p (fun x ↦ ext_dom.definedAtLeft x) (fun y ↦ ext_cod.definedAtRight y)

Result:
case mk.intro.intro.mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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 : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝³ : Countable ↑X
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p => Sum.recOn p (fun x => ext_dom.definedAtLeft ↑x) fun y => ext_cod.definedAtRight ↑y
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Proof state:
case mk.intro.intro.mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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 : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝⁵ : Countable ↑X
x✝⁴ : Encodable ↑X
x✝³ : Countable ↑Y
x✝² : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p => Sum.recOn p (fun x => ext_dom.definedAtLeft ↑x) fun y => ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝¹ : X ⊆ ↑F.dom
x✝ : Y ⊆ ↑F.cod
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
have dom_top : F.dom = ⊤ := by rwa [← top_le_iff, ← X_gen, Substructure.closure_le]

Result:
case mk.intro.intro.mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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 : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝⁵ : Countable ↑X
x✝⁴ : Encodable ↑X
x✝³ : Countable ↑Y
x✝² : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p => Sum.recOn p (fun x => ext_dom.definedAtLeft ↑x) fun y => ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝¹ : X ⊆ ↑F.dom
x✝ : Y ⊆ ↑F.cod
dom_top : F.dom = ⊤
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Proof state:
case mk.intro.intro.mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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 : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝² : Countable ↑X
x✝¹ : Encodable ↑X
x✝ : Countable ↑Y
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
have _ : Encodable (↑Y : Type _) := Encodable.ofCountable _

Result:
case mk.intro.intro.mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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 : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝³ : Countable ↑X
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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 : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝³ : Countable ↑X
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p => Sum.recOn p (fun x => ext_dom.definedAtLeft ↑x) fun y => ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x : M
hx : x ∈ X
⊢ x ∈ ↑F.dom

Tactic:
have := Order.sequenceOfCofinals.encode_mem g D (Sum.inl ⟨x, hx⟩)

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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 : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝³ : Countable ↑X
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p => Sum.recOn p (fun x => ext_dom.definedAtLeft ↑x) fun y => ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x : M
hx : x ∈ X
this : Order.sequenceOfCofinals g D (Encodable.encode (Sum.inl ⟨x, hx⟩) + 1) ∈ D (Sum.inl ⟨x, hx⟩)
⊢ x ∈ ↑F.dom

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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 : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝⁵ : Countable ↑X
x✝⁴ : Encodable ↑X
x✝³ : Countable ↑Y
x✝² : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p => Sum.recOn p (fun x => ext_dom.definedAtLeft ↑x) fun y => ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝¹ : X ⊆ ↑F.dom
x✝ : Y ⊆ ↑F.cod
dom_top : F.dom = ⊤
⊢ F.cod = ⊤

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

Result:
no goals