awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w
inst : Language.order.Structure M
inst_1 : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst_2 : Language.order.Structure N
inst_3 : N ⊨ Language.order.dlo
inst_4 : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : Embedding.{0, 0, w, w'} Language.order (↥S) N
m : M
this_1 : LinearOrder M := Language.order.linearOrderOfModels M
this_2 : LinearOrder N := Language.order.linearOrderOfModels N
this_3 : DenselyOrdered N
this_4 : NoBotOrder N
this_5 : NoTopOrder N
this_6 : NoMinOrder N
this : NoMaxOrder N
hS : (↑S : Set M).Finite
g : OrderEmbedding.{w, w'} (↥(insert m (hS.toFinset (s := (↑S : Set M))))) N
hg :
  Eq (α := (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w) → N)
    (Function.comp (β := ↥(insert m (hS.toFinset (s := (↑S : Set M))))) (⇑g : (a : ↥(insert m hS.toFinset)) → N)
      (Set.inclusion (s := (↑(hS.toFinset (s := (↑S : Set M))) : Set M)) (t :=
        (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)) ⋯))
    (⇑(RelEmbedding.trans (r := fun (x1 x2 : (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w)) ↦ x1 ≤ x2) (s :=
          fun (x1 x2 : (↑(↑S : Set M) : Type w)) ↦ x1 ≤ x2) (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
          (OrderIso.toOrderEmbedding (OrderIso.setCongr (↑(hS.toFinset (s := (↑S : Set M))) : Set M) (↑S : Set M) ⋯))
          (OrderEmbedding.ofStrictMono (⇑f : (a : ↥S) → N) ⋯)) :
      (a : ↥hS.toFinset) → N)
h :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S =
    LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order)
      (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)
⊢ (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M) =
    (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)

Tactic:
convert!
        LowerAdjoint.closure_eq_self_of_mem_closed _
          (Substructure.mem_closed_of_isRelational Language.order
            ((insert m hS.toFinset : Finset M) : Set M))

Premises used: Insert.insert, FirstOrder.Language.Substructure.mem_closed_of_isRelational, SetLike.coe, Set.Finite.toFinset, FirstOrder.Language.order, LowerAdjoint.closure_eq_self_of_mem_closed
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w
inst : Language.order.Structure M
inst_1 : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst_2 : Language.order.Structure N
inst_3 : N ⊨ Language.order.dlo
inst_4 : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : Embedding.{0, 0, w, w'} Language.order (↥S) N
m : M
this_1 : LinearOrder M := Language.order.linearOrderOfModels M
this_2 : LinearOrder N := Language.order.linearOrderOfModels N
this_3 : DenselyOrdered N
this_4 : NoBotOrder N
this_5 : NoTopOrder N
this_6 : NoMinOrder N
this : NoMaxOrder N
hS : (↑S : Set M).Finite
g : OrderEmbedding.{w, w'} (↥(insert m (hS.toFinset (s := (↑S : Set M))))) N
hg :
  Eq (α := (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w) → N)
    (Function.comp (β := ↥(insert m (hS.toFinset (s := (↑S : Set M))))) (⇑g : (a : ↥(insert m hS.toFinset)) → N)
      (Set.inclusion (s := (↑(hS.toFinset (s := (↑S : Set M))) : Set M)) (t :=
        (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)) ⋯))
    (⇑(RelEmbedding.trans (r := fun (x1 x2 : (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w)) ↦ x1 ≤ x2) (s :=
          fun (x1 x2 : (↑(↑S : Set M) : Type w)) ↦ x1 ≤ x2) (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
          (OrderIso.toOrderEmbedding (OrderIso.setCongr (↑(hS.toFinset (s := (↑S : Set M))) : Set M) (↑S : Set M) ⋯))
          (OrderEmbedding.ofStrictMono (⇑f : (a : ↥S) → N) ⋯)) :
      (a : ↥hS.toFinset) → N)
⊢ LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S =
    LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order)
      (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)

Tactic:
simp only [Finset.coe_insert, Set.Finite.coe_toFinset, Substructure.closure_insert,
        Substructure.closure_eq]

Premises used: Set.Finite.coe_toFinset, FirstOrder.Language.Substructure.closure_insert, Finset.coe_insert, FirstOrder.Language.Substructure.closure_eq
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w
inst : Language.order.Structure M
inst_1 : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst_2 : Language.order.Structure N
inst_3 : N ⊨ Language.order.dlo
inst_4 : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : Embedding.{0, 0, w, w'} Language.order (↥S) N
m : M
this_1 : LinearOrder M := Language.order.linearOrderOfModels M
this_2 : LinearOrder N := Language.order.linearOrderOfModels N
this_3 : DenselyOrdered N
this_4 : NoBotOrder N
this_5 : NoTopOrder N
this_6 : NoMinOrder N
this : NoMaxOrder N
hS : (↑S : Set M).Finite
g : OrderEmbedding.{w, w'} (↥(insert m (hS.toFinset (s := (↑S : Set M))))) N
hg :
  Eq (α := (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w) → N)
    (Function.comp (β := ↥(insert m (hS.toFinset (s := (↑S : Set M))))) (⇑g : (a : ↥(insert m hS.toFinset)) → N)
      (Set.inclusion (s := (↑(hS.toFinset (s := (↑S : Set M))) : Set M)) (t :=
        (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)) ⋯))
    (⇑(RelEmbedding.trans (r := fun (x1 x2 : (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w)) ↦ x1 ≤ x2) (s :=
          fun (x1 x2 : (↑(↑S : Set M) : Type w)) ↦ x1 ≤ x2) (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
          (OrderIso.toOrderEmbedding (OrderIso.setCongr (↑(hS.toFinset (s := (↑S : Set M))) : Set M) (↑S : Set M) ⋯))
          (OrderEmbedding.ofStrictMono (⇑f : (a : ↥S) → N) ⋯)) :
      (a : ↥hS.toFinset) → N)
g' : OrderEmbedding.{w, w'} (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S))
  N :=
  RelEmbedding.trans (r :=
    fun
      (x1 x2 :
        (↑(↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M) : Type w)) ↦
    x1 ≤ x2) (s := fun (x1 x2 : (↑(↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) : Type w)) ↦ x1 ≤ x2) (t :=
    fun (x1 x2 : N) ↦ x1 ≤ x2)
    (OrderIso.toOrderEmbedding
      (OrderIso.setCongr
        (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M)
        (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) ⋯))
    g
h : f = Embedding.comp (StrongHomClass.toEmbedding g') (Substructure.inclusion ⋯)
⊢ ∃ (g :
    Embedding.{0, 0, w, w'} Language.order
      (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S)) N),
    f = g.comp (Substructure.inclusion ⋯)

Tactic:
use StrongHomClass.toEmbedding g'

Premises used: FirstOrder.Language.StrongHomClass.toEmbedding
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w
inst : Language.order.Structure M
inst_1 : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst_2 : Language.order.Structure N
inst_3 : N ⊨ Language.order.dlo
inst_4 : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : Embedding.{0, 0, w, w'} Language.order (↥S) N
m : M
this_1 : LinearOrder M := Language.order.linearOrderOfModels M
this_2 : LinearOrder N := Language.order.linearOrderOfModels N
this_3 : DenselyOrdered N
this_4 : NoBotOrder N
this_5 : NoTopOrder N
this_6 : NoMinOrder N
this : NoMaxOrder N
hS : (↑S : Set M).Finite
g : OrderEmbedding.{w, w'} (↥(insert m (hS.toFinset (s := (↑S : Set M))))) N
hg :
  Eq (α := (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w) → N)
    (Function.comp (β := ↥(insert m (hS.toFinset (s := (↑S : Set M))))) (⇑g : (a : ↥(insert m hS.toFinset)) → N)
      (Set.inclusion (s := (↑(hS.toFinset (s := (↑S : Set M))) : Set M)) (t :=
        (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)) ⋯))
    (⇑(RelEmbedding.trans (r := fun (x1 x2 : (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w)) ↦ x1 ≤ x2) (s :=
          fun (x1 x2 : (↑(↑S : Set M) : Type w)) ↦ x1 ≤ x2) (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
          (OrderIso.toOrderEmbedding (OrderIso.setCongr (↑(hS.toFinset (s := (↑S : Set M))) : Set M) (↑S : Set M) ⋯))
          (OrderEmbedding.ofStrictMono (⇑f : (a : ↥S) → N) ⋯)) :
      (a : ↥hS.toFinset) → N)
g' : OrderEmbedding.{w, w'} (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S))
  N :=
  RelEmbedding.trans (r :=
    fun
      (x1 x2 :
        (↑(↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M) : Type w)) ↦
    x1 ≤ x2) (s := fun (x1 x2 : (↑(↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) : Type w)) ↦ x1 ≤ x2) (t :=
    fun (x1 x2 : N) ↦ x1 ≤ x2)
    (OrderIso.toOrderEmbedding
      (OrderIso.setCongr
        (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M)
        (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) ⋯))
    g
h :
  ∀ (x : M) (xS : x ∈ S),
    Eq.{w' + 1} (α := N) ((f : (a : ↥S) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xS) : N)
      ((Embedding.comp (StrongHomClass.toEmbedding g') (Substructure.inclusion ⋯) : (a : ↥S) → N)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xS) :
        N)
⊢ f = Embedding.comp (StrongHomClass.toEmbedding g') (Substructure.inclusion ⋯)

Tactic:
ext ⟨x, xS⟩
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w
inst : Language.order.Structure M
inst_1 : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst_2 : Language.order.Structure N
inst_3 : N ⊨ Language.order.dlo
inst_4 : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : Embedding.{0, 0, w, w'} Language.order (↥S) N
m : M
this_1 : LinearOrder M := Language.order.linearOrderOfModels M
this_2 : LinearOrder N := Language.order.linearOrderOfModels N
this_3 : DenselyOrdered N
this_4 : NoBotOrder N
this_5 : NoTopOrder N
this_6 : NoMinOrder N
this : NoMaxOrder N
hS : (↑S : Set M).Finite
g : OrderEmbedding.{w, w'} (↥(insert m (hS.toFinset (s := (↑S : Set M))))) N
hg :
  Eq (α := (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w) → N)
    (Function.comp (β := ↥(insert m (hS.toFinset (s := (↑S : Set M))))) (⇑g : (a : ↥(insert m hS.toFinset)) → N)
      (Set.inclusion (s := (↑(hS.toFinset (s := (↑S : Set M))) : Set M)) (t :=
        (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)) ⋯))
    (⇑(RelEmbedding.trans (r := fun (x1 x2 : (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w)) ↦ x1 ≤ x2) (s :=
          fun (x1 x2 : (↑(↑S : Set M) : Type w)) ↦ x1 ≤ x2) (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
          (OrderIso.toOrderEmbedding (OrderIso.setCongr (↑(hS.toFinset (s := (↑S : Set M))) : Set M) (↑S : Set M) ⋯))
          (OrderEmbedding.ofStrictMono (⇑f : (a : ↥S) → N) ⋯)) :
      (a : ↥hS.toFinset) → N)
g' : OrderEmbedding.{w, w'} (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S))
  N :=
  RelEmbedding.trans (r :=
    fun
      (x1 x2 :
        (↑(↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M) : Type w)) ↦
    x1 ≤ x2) (s := fun (x1 x2 : (↑(↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) : Type w)) ↦ x1 ≤ x2) (t :=
    fun (x1 x2 : N) ↦ x1 ≤ x2)
    (OrderIso.toOrderEmbedding
      (OrderIso.setCongr
        (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M)
        (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) ⋯))
    g
x : M
xS : x ∈ S
⊢ Eq.{w' + 1} (α := N) ((f : (a : ↥S) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xS) : N)
    ((Embedding.comp (StrongHomClass.toEmbedding g') (Substructure.inclusion ⋯) : (a : ↥S) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xS) :
      N)

Tactic:
congr_fun hg.symm ⟨x, (?_ : x ∈ hS.toFinset)⟩

Premises used: Subtype.mk, congr_fun, Eq.symm
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w
inst : Language.order.Structure M
inst_1 : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst_2 : Language.order.Structure N
inst_3 : N ⊨ Language.order.dlo
inst_4 : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : Embedding.{0, 0, w, w'} Language.order (↥S) N
m : M
this_1 : LinearOrder M := Language.order.linearOrderOfModels M
this_2 : LinearOrder N := Language.order.linearOrderOfModels N
this_3 : DenselyOrdered N
this_4 : NoBotOrder N
this_5 : NoTopOrder N
this_6 : NoMinOrder N
this : NoMaxOrder N
hS : (↑S : Set M).Finite
g : OrderEmbedding.{w, w'} (↥(insert m (hS.toFinset (s := (↑S : Set M))))) N
hg :
  Eq (α := (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w) → N)
    (Function.comp (β := ↥(insert m (hS.toFinset (s := (↑S : Set M))))) (⇑g : (a : ↥(insert m hS.toFinset)) → N)
      (Set.inclusion (s := (↑(hS.toFinset (s := (↑S : Set M))) : Set M)) (t :=
        (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)) ⋯))
    (⇑(RelEmbedding.trans (r := fun (x1 x2 : (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w)) ↦ x1 ≤ x2) (s :=
          fun (x1 x2 : (↑(↑S : Set M) : Type w)) ↦ x1 ≤ x2) (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
          (OrderIso.toOrderEmbedding (OrderIso.setCongr (↑(hS.toFinset (s := (↑S : Set M))) : Set M) (↑S : Set M) ⋯))
          (OrderEmbedding.ofStrictMono (⇑f : (a : ↥S) → N) ⋯)) :
      (a : ↥hS.toFinset) → N)
g' : OrderEmbedding.{w, w'} (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S))
  N :=
  RelEmbedding.trans (r :=
    fun
      (x1 x2 :
        (↑(↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M) : Type w)) ↦
    x1 ≤ x2) (s := fun (x1 x2 : (↑(↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) : Type w)) ↦ x1 ≤ x2) (t :=
    fun (x1 x2 : N) ↦ x1 ≤ x2)
    (OrderIso.toOrderEmbedding
      (OrderIso.setCongr
        (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M)
        (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) ⋯))
    g
x : M
xS : x ∈ S
h : x ∈ hS.toFinset (s := (↑S : Set M))
⊢ Eq.{w' + 1} (α := N) ((f : (a : ↥S) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xS) : N)
    ((Embedding.comp (StrongHomClass.toEmbedding g') (Substructure.inclusion ⋯) : (a : ↥S) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xS) :
      N)

Tactic:
refine congr_fun hg.symm ⟨x, (?_ : x ∈ hS.toFinset)⟩

Premises used: Subtype.mk, congr_fun, Eq.symm
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w
inst : Language.order.Structure M
inst_1 : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst_2 : Language.order.Structure N
inst_3 : N ⊨ Language.order.dlo
inst_4 : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : Embedding.{0, 0, w, w'} Language.order (↥S) N
m : M
this_1 : LinearOrder M := Language.order.linearOrderOfModels M
this_2 : LinearOrder N := Language.order.linearOrderOfModels N
this_3 : DenselyOrdered N
this_4 : NoBotOrder N
this_5 : NoTopOrder N
this_6 : NoMinOrder N
this : NoMaxOrder N
hS : (↑S : Set M).Finite
g : OrderEmbedding.{w, w'} (↥(insert m (hS.toFinset (s := (↑S : Set M))))) N
hg :
  Eq (α := (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w) → N)
    (Function.comp (β := ↥(insert m (hS.toFinset (s := (↑S : Set M))))) (⇑g : (a : ↥(insert m hS.toFinset)) → N)
      (Set.inclusion (s := (↑(hS.toFinset (s := (↑S : Set M))) : Set M)) (t :=
        (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)) ⋯))
    (⇑(RelEmbedding.trans (r := fun (x1 x2 : (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w)) ↦ x1 ≤ x2) (s :=
          fun (x1 x2 : (↑(↑S : Set M) : Type w)) ↦ x1 ≤ x2) (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
          (OrderIso.toOrderEmbedding (OrderIso.setCongr (↑(hS.toFinset (s := (↑S : Set M))) : Set M) (↑S : Set M) ⋯))
          (OrderEmbedding.ofStrictMono (⇑f : (a : ↥S) → N) ⋯)) :
      (a : ↥hS.toFinset) → N)
g' : OrderEmbedding.{w, w'} (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S))
  N :=
  RelEmbedding.trans (r :=
    fun
      (x1 x2 :
        (↑(↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M) : Type w)) ↦
    x1 ≤ x2) (s := fun (x1 x2 : (↑(↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) : Type w)) ↦ x1 ≤ x2) (t :=
    fun (x1 x2 : N) ↦ x1 ≤ x2)
    (OrderIso.toOrderEmbedding
      (OrderIso.setCongr
        (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M)
        (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) ⋯))
    g
x : M
xS : x ∈ S
⊢ x ∈ hS.toFinset (s := (↑S : Set M))

Tactic:
simp only [Set.Finite.mem_toFinset, SetLike.mem_coe, xS]

Premises used: Set.Finite.mem_toFinset, SetLike.mem_coe
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M_1 : Type w'
n : ℕ
M : Type w
inst : Language.order.Structure M
inst_1 : M ⊨ Language.order.dlo
inst_2 : Nonempty M
this : Language.order.Structure ℚ := orderStructure ℚ
obtain : ∀ (f : ℚ ↪[Language.order] M), (↑default : ℚ ≃ₚ[Language.order] M) ≤ f.toPartialEquiv → Infinite M
⊢ Infinite M

Tactic:
obtain ⟨f, _⟩ := embedding_from_cg cg_of_countable default (dlo_isExtensionPair ℚ M)

Premises used: Inhabited.default, Rat, FirstOrder.Language.embedding_from_cg, FirstOrder.Language.dlo_isExtensionPair, FirstOrder.Language.Structure.cg_of_countable
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M_1 : Type w'
n : ℕ
M : Type w
inst : Language.order.Structure M
inst_1 : M ⊨ Language.order.dlo
inst_2 : Nonempty M
this : Language.order.Structure ℚ := orderStructure ℚ
f : ℚ ↪[Language.order] M
h : (↑default : ℚ ≃ₚ[Language.order] M) ≤ f.toPartialEquiv
⊢ Infinite M

Tactic:
Infinite.of_injective f f.injective

Premises used: Infinite.of_injective, FirstOrder.Language.Embedding.injective, DFunLike.coe
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M_1 : Type w'
n : ℕ
M : Type w
inst : Language.order.Structure M
inst_1 : M ⊨ Language.order.dlo
inst_2 : Nonempty M
this : Language.order.Structure ℚ := orderStructure ℚ
f : ℚ ↪[Language.order] M
h : (↑default : ℚ ≃ₚ[Language.order] M) ≤ f.toPartialEquiv
⊢ Infinite M

Tactic:
exact Infinite.of_injective f f.injective

Premises used: Infinite.of_injective, FirstOrder.Language.Embedding.injective, DFunLike.coe
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w'
inst : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst_1 : Nonempty M
h :
  ∀ (N : CategoryTheory.Bundled Language.order.Structure),
    Membership.mem (γ := Set (CategoryTheory.Bundled Language.order.Structure))
        {N : CategoryTheory.Bundled Language.order.Structure |
          FG.{w', 0, 0} Language.order (↑N : Type w') ∧ Nonempty.{w' + 1} ((↑N : Type w') ↪[Language.order] M)}
        N ↔
      Membership.mem (γ := Set (CategoryTheory.Bundled Language.order.Structure))
        {M : CategoryTheory.Bundled Language.order.Structure |
          Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}
        N
⊢ Eq.{w' + 2} (α := Set (CategoryTheory.Bundled Language.order.Structure))
    {N : CategoryTheory.Bundled Language.order.Structure |
      FG.{w', 0, 0} Language.order (↑N : Type w') ∧ Nonempty.{w' + 1} ((↑N : Type w') ↪[Language.order] M)}
    {M : CategoryTheory.Bundled Language.order.Structure |
      Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}

Tactic:
ext N
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w'
inst : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst_1 : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
⊢ Membership.mem (γ := Set (CategoryTheory.Bundled Language.order.Structure))
      {N : CategoryTheory.Bundled Language.order.Structure |
        FG.{w', 0, 0} Language.order (↑N : Type w') ∧ Nonempty.{w' + 1} ((↑N : Type w') ↪[Language.order] M)}
      N ↔
    Membership.mem (γ := Set (CategoryTheory.Bundled Language.order.Structure))
      {M : CategoryTheory.Bundled Language.order.Structure |
        Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}
      N

Tactic:
⟨fun ⟨hF, h⟩ => ⟨hF.finite, Theory.IsUniversal.models_of_embedding h.some⟩,
    fun ⟨hF, h⟩ => ⟨FG.of_finite, ?_⟩⟩

Premises used: _private.0.FirstOrder.Language.dlo_age.match_2, Finite, FirstOrder.Language.Structure.FG.finite, setOf, Membership.mem, FirstOrder.Language.Theory.IsUniversal.models_of_embedding, Nonempty.some, FirstOrder.Language.Theory.Model, FirstOrder.Language.Embedding, FirstOrder.Language.Structure.FG, And, CategoryTheory.Bundled.α, FirstOrder.Language.linearOrderTheory, And.intro, FirstOrder.Language.order, Iff.intro, Nonempty, _private.0.FirstOrder.Language.dlo_age.match_1, FirstOrder.Language.Structure.FG.of_finite
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w'
inst : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst_1 : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
h :
  Membership.mem (γ := Set (CategoryTheory.Bundled Language.order.Structure))
      {M : CategoryTheory.Bundled Language.order.Structure |
        Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}
      N →
    ∀ (hF : Finite.{w' + 1} (↑N : Type w'))
      (h : Theory.Model.{0, 0, w'} (↑N : Type w') Language.order.linearOrderTheory),
      Nonempty.{w' + 1} ((↑N : Type w') ↪[Language.order] M)
⊢ Membership.mem (γ := Set (CategoryTheory.Bundled Language.order.Structure))
      {N : CategoryTheory.Bundled Language.order.Structure |
        FG.{w', 0, 0} Language.order (↑N : Type w') ∧ Nonempty.{w' + 1} ((↑N : Type w') ↪[Language.order] M)}
      N ↔
    Membership.mem (γ := Set (CategoryTheory.Bundled Language.order.Structure))
      {M : CategoryTheory.Bundled Language.order.Structure |
        Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}
      N

Tactic:
refine ⟨fun ⟨hF, h⟩ => ⟨hF.finite, Theory.IsUniversal.models_of_embedding h.some⟩,
    fun ⟨hF, h⟩ => ⟨FG.of_finite, ?_⟩⟩
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w'
inst : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst_1 : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
h_1 :
  Membership.mem (γ := Set (CategoryTheory.Bundled Language.order.Structure))
    {M : CategoryTheory.Bundled Language.order.Structure |
      Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}
    N
hF : Finite.{w' + 1} (↑N : Type w')
h : Theory.Model.{0, 0, w'} (↑N : Type w') Language.order.linearOrderTheory
this_1 : LinearOrder M := Language.order.linearOrderOfModels M
this : LinearOrder (↑N : Type w') := Language.order.linearOrderOfModels (↑N : Type w')
⊢ Nonempty.{w' + 1} ((↑N : Type w') ↪[Language.order] M)

Tactic:
⟨StrongHomClass.toEmbedding (nonempty_orderEmbedding_of_finite_infinite N M).some⟩

Premises used: FirstOrder.Language.StrongHomClass.toEmbedding, nonempty_orderEmbedding_of_finite_infinite, Nonempty.some, Nonempty.intro, CategoryTheory.Bundled.α
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w'
inst : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst_1 : Nonempty M
N : CategoryTheory.Bundled Language.order.Structure
h_1 :
  Membership.mem (γ := Set (CategoryTheory.Bundled Language.order.Structure))
    {M : CategoryTheory.Bundled Language.order.Structure |
      Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}
    N
hF : Finite.{w' + 1} (↑N : Type w')
h : Theory.Model.{0, 0, w'} (↑N : Type w') Language.order.linearOrderTheory
this_1 : LinearOrder M := Language.order.linearOrderOfModels M
this : LinearOrder (↑N : Type w') := Language.order.linearOrderOfModels (↑N : Type w')
⊢ Nonempty.{w' + 1} ((↑N : Type w') ↪[Language.order] M)

Tactic:
exact ⟨StrongHomClass.toEmbedding (nonempty_orderEmbedding_of_finite_infinite N M).some⟩