-- 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
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝ : X ⊆ ↑F.dom
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

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

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
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
rcases M_cg with ⟨X, X_count, X_gen⟩

Result:
case mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : 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 : (closure L).toFun X = ⊤
⊢ ∃ 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 = ⊤
⊢ Countable ↑X

Tactic:
simpa only [countable_coe_iff]

Result:
no goals

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, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
let F := @DirectLimit.partialEquivLimit L M N _ _ ℕ _ _ _ S

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
⊢ ∃ 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
this : Order.sequenceOfCofinals g D (Encodable.encode (Sum.inl ⟨x, hx⟩) + 1) ∈ D (Sum.inl ⟨x, hx⟩)
⊢ x ∈ ↑F.dom

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

Result:
no goals

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
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
have _ : Encodable (↑X : 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
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Proof state:
case h.e'_4
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 = ⊤
cod_top : F.cod = ⊤
⊢ (toEquivOfEqTop dom_top cod_top).toEmbedding.toPartialEquiv = partialEquivLimit S

Tactic:
rw [toEquivOfEqTop_toEmbedding]

Result:
case h.e'_4
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 = ⊤
cod_top : F.cod = ⊤
⊢ (toEmbeddingOfEqTop dom_top).toPartialEquiv = partialEquivLimit S