-- Mathlib/ModelTheory/PartialEquiv.lean
theorem embedding_from_cg (M_cg : Structure.CG L M) (g : L.FGEquiv M N)
    (H : L.IsExtensionPair M N) :
    ∃ f : M ↪[L] N, g ≤ f.toPartialEquiv

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝² : Countable ↑X
x✝¹ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x => H.definedAtLeft ↑x
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝ : X ⊆ ↑F.dom
⊢ F.dom = ⊤

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

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
⊢ Countable ↑X

Tactic:
simpa only [countable_coe_iff]

Result:
no goals

Proof state:
case mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
⊢ ∃ f, ↑g ≤ f.toPartialEquiv

Tactic:
have _ : Countable (↑X : Type _) := by simpa only [countable_coe_iff]

Result:
case mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝ : Countable ↑X
⊢ ∃ f, ↑g ≤ f.toPartialEquiv

Proof state:
case mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝² : Countable ↑X
x✝¹ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x => H.definedAtLeft ↑x
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.toPartialEquiv

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

Result:
case mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝² : Countable ↑X
x✝¹ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x => H.definedAtLeft ↑x
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝ : X ⊆ ↑F.dom
isTop : F.dom = ⊤
⊢ ∃ f, ↑g ≤ f.toPartialEquiv

Proof state:
case mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝¹ : Countable ↑X
x✝ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x => H.definedAtLeft ↑x
⊢ ∃ f, ↑g ≤ f.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
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝¹ : Countable ↑X
x✝ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x => H.definedAtLeft ↑x
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
⊢ ∃ f, ↑g ≤ f.toPartialEquiv

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝¹ : Countable ↑X
x✝ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x => H.definedAtLeft ↑x
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 ⟨x, hx⟩

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝¹ : Countable ↑X
x✝ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x => H.definedAtLeft ↑x
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 ⟨x, hx⟩ + 1) ∈ D ⟨x, hx⟩
⊢ x ∈ ↑F.dom

Proof state:
case mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝² : Countable ↑X
x✝¹ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x => H.definedAtLeft ↑x
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝ : X ⊆ ↑F.dom
isTop : F.dom = ⊤
⊢ ∃ f, ↑g ≤ f.toPartialEquiv

Tactic:
exact ⟨toEmbeddingOfEqTop isTop,
      by convert (le_partialEquivLimit S 0); apply Embedding.toPartialEquiv_toEmbedding⟩

Result:
no goals