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
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : Embedding.{u, v, w, w'} L (↥S) N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom
ff'1 :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
            { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
        M ≃ₚ[L] N).dom ≤
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom
ff'2 :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).cod.subtype.comp
      ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).toEquiv.toEmbedding.comp
        (Substructure.inclusion ff'1)) =
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                  { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
              M ≃ₚ[L] N).cod.subtype.comp
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) { dom := S, cod := f.toHom.range, toEquiv := f.equivRange }
                S_FG) :
            M ≃ₚ[L] N).toEquiv.toEmbedding
x : M
hx : x ∈ S
refine_1 :
  ∀
    (ff'2 :
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).cod.subtype.comp
          ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).toEquiv.toEmbedding.comp
            (Substructure.inclusion ff'1)) =
        f)
    (x : M) (hx : x ∈ S),
    Eq.{w' + 1} (α := N) ((f : (a : ↥S) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) : N)
      ((Embedding.comp (N := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S))
              (f'.toEmbedding.comp (Substructure.inclusion ⋯)) (Substructure.inclusion ⋯) :
            (a : ↥S) → N)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) :
        N)
⊢ Eq.{w' + 1} (α := N) ((f : (a : ↥S) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) : N)
    ((Embedding.comp (N := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S))
            (f'.toEmbedding.comp (Substructure.inclusion ⋯)) (Substructure.inclusion ⋯) :
          (a : ↥S) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) :
      N)

Tactic:
rw [Embedding.subtype_equivRange] at ff'2

Premises used: FirstOrder.Language.Embedding.subtype_equivRange
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : Embedding.{u, v, w, w'} L (↥S) N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom
ff'1 :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
            { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
        M ≃ₚ[L] N).dom ≤
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom
ff'2 :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).cod.subtype.comp
      ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).toEquiv.toEmbedding.comp
        (Substructure.inclusion ff'1)) =
    f
x : M
hx : x ∈ S
⊢ Eq.{w' + 1} (α := N) ((f : (a : ↥S) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) : N)
    ((Embedding.comp (N := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S))
            (f'.toEmbedding.comp (Substructure.inclusion ⋯)) (Substructure.inclusion ⋯) :
          (a : ↥S) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) :
      N)

Tactic:
simp only [← ff'2, Embedding.comp_apply, Substructure.coe_inclusion, inclusion_mk,
        Equiv.coe_toEmbedding, coe_subtype, PartialEquiv.toEmbedding_apply]

Premises used: FirstOrder.Language.PartialEquiv.toEmbedding_apply, FirstOrder.Language.Substructure.coe_inclusion, FirstOrder.Language.Substructure.coe_subtype, FirstOrder.Language.Embedding.comp_apply, Set.inclusion_mk, FirstOrder.Language.Equiv.coe_toEmbedding
-- Module: Mathlib.ModelTheory.PartialEquiv
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
refine_2 :
  ∀ (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
⊢ ∃ (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

Tactic:
obtain ⟨f', eq_f'⟩ := h f.dom f_FG f.toEmbedding m

Premises used: FirstOrder.Language.PartialEquiv.toEmbedding, FirstOrder.Language.PartialEquiv.dom
-- Module: Mathlib.ModelTheory.PartialEquiv
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

Tactic:
⟨⟨⟨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 _ => ?_)⟩⟩

Premises used: Set.mem_singleton, FirstOrder.Language.Substructure.fg_closure_singleton, le_sup_left, FirstOrder.Language.PartialEquiv.dom, HasSubset.Subset.trans, le_sup_right, Subtype.mk, FirstOrder.Language.Hom.range, FirstOrder.Language.Embedding.equivRange, FirstOrder.Language.PartialEquiv.mk, FirstOrder.Language.Substructure.subset_closure, Max.max, FirstOrder.Language.Substructure.FG.sup, And.intro, Exists.intro, LowerAdjoint.toFun, FirstOrder.Language.Substructure.closure, FirstOrder.Language.Embedding.ext, Singleton.singleton, FirstOrder.Language.Embedding.toHom
-- Module: Mathlib.ModelTheory.PartialEquiv
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 ⋯)
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 }
                          ⋯) :
                      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 :
        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)
⊢ ∃ (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

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 _ => ?_)⟩⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
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
refine_2 :
  ∀ (eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion ⋯))
    (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 }
                          ⋯) :
                      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 :
        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)
⊢ 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)

Tactic:
rw [PartialEquiv.toEmbedding] at eq_f'

Premises used: FirstOrder.Language.PartialEquiv.toEmbedding
-- Module: Mathlib.ModelTheory.PartialEquiv
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.cod.subtype.comp f.toEquiv.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)

Tactic:
simp only [Embedding.comp_apply, Substructure.coe_inclusion, Equiv.coe_toEmbedding, coe_subtype,
      Embedding.equivRange_apply, eq_f']

Premises used: FirstOrder.Language.Substructure.coe_inclusion, FirstOrder.Language.Substructure.coe_subtype, FirstOrder.Language.Embedding.comp_apply, FirstOrder.Language.Equiv.coe_toEmbedding, FirstOrder.Language.Embedding.equivRange_apply
-- 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
g : L.FGEquiv M N
H : L.IsExtensionPair M N
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
⊢ ∃ (f : M ↪[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toPartialEquiv

Tactic:
rcases M_cg with ⟨X, _, X_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
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) ⊤
⊢ 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
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) ⊤
⊢ 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
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)
have : ∀ (x : Encodable (↑X : Type w)), ∃ (f : M ↪[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toPartialEquiv
⊢ ∃ (f : M ↪[L] N), (↑g : M ≃ₚ[L] N) ≤ f.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
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
⊢ 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⟩
-- 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_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
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)
⊢ x ∈ (↑F.dom : Set M)

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

Premises used: FirstOrder.Language.PartialEquiv.dom_le_dom, Set.Mem, 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
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
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)
⊢ x ∈ (↑F.dom : Set M)

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

Premises used: FirstOrder.Language.PartialEquiv.dom_le_dom, 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
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
⊢ 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
-- 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)
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
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 = ⊤

Tactic:
have isTop : 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
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 = ⊤
⊢ (S : (a : ℕ) → M ≃ₚ[L] N) 0 ≤ partialEquivLimit S

Tactic:
(le_partialEquivLimit S 0)

Premises used: 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
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_1 : 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_2 : X ⊆ (↑F.dom : Set M)
isTop : F.dom = ⊤
h : (toEmbeddingOfEqTop isTop).toPartialEquiv = partialEquivLimit S
⊢ (↑g : M ≃ₚ[L] N) ≤ (toEmbeddingOfEqTop isTop).toPartialEquiv

Tactic:
convert! (le_partialEquivLimit S 0)

Premises used: 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
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 = ⊤
⊢ (toEmbeddingOfEqTop isTop).toPartialEquiv = partialEquivLimit S

Tactic:
apply Embedding.toPartialEquiv_toEmbedding

Premises used: FirstOrder.Language.Embedding.toPartialEquiv_toEmbedding