awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
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) : Set M) =
    (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)
have 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)
Tactic: convert!
        LowerAdjoint.closure_eq_self_of_mem_closed _
          (Substructure.mem_closed_of_isRelational Language.order
            ((insert m hS.toFinset : Finset M) : Set M))
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
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
⊢ ∃ (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 ⋯)
have h : f = Embedding.comp (StrongHomClass.toEmbedding g') (Substructure.inclusion sorry)
Tactic: use StrongHomClass.toEmbedding g'
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
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
⊢ f = Embedding.comp (StrongHomClass.toEmbedding g') (Substructure.inclusion ⋯)
have 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 sorry) : (a : ↥S) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xS) :
      N)
Tactic: ext ⟨x, xS⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
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)
have h : x ∈ hS.toFinset (s := (↑S : Set M))
Tactic: refine congr_fun hg.symm ⟨x, (?_ : x ∈ hS.toFinset)⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
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
⊢ Language.order.IsExtensionPair M N
have rw : ∀ (S : Language.order.Substructure M),
  S.FG →
    ∀ (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
      ∃ (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 sorry)
Tactic: classical
  rw [isExtensionPair_iff_exists_embedding_closure_singleton_sup]
  intro S S_fg f m
  letI := Language.order.linearOrderOfModels M
  letI := Language.order.linearOrderOfModels N
  have := Language.order.denselyOrdered_of_dlo N
  have := Language.order.noBotOrder_of_dlo N
  have := Language.order.noTopOrder_of_dlo N
  have := NoBotOrder.to_noMinOrder N
  have := NoTopOrder.to_noMaxOrder N
  have hS : Set.Finite (S : Set M) := (S.fg_iff_structure_fg.1 S_fg).finite
  obtain ⟨g, hg⟩ := Order.exists_orderEmbedding_insert hS.toFinset
    ((OrderIso.setCongr hS.toFinset (S : Set M) hS.coe_toFinset).toOrderEmbedding.trans
      (OrderEmbedding.ofStrictMono f (HomClass.strictMono f))) m
  let g' :
    ((Substructure.closure Language.order).toFun {m} ⊔ S : Language.order.Substructure M) ↪o N :=
    ((OrderIso.setCongr _ _ (by
      convert!
        LowerAdjoint.closure_eq_self_of_mem_closed _
          (Substructure.mem_closed_of_isRelational Language.order
            ((insert m hS.toFinset : Finset M) : Set M))
      simp only [Finset.coe_insert, Set.Finite.coe_toFinset, Substructure.closure_insert,
        Substructure.closure_eq])).toOrderEmbedding.trans g)
  use StrongHomClass.toEmbedding g'
  ext ⟨x, xS⟩
  refine congr_fun hg.symm ⟨x, (?_ : x ∈ hS.toFinset)⟩
  simp only [Set.Finite.mem_toFinset, SetLike.mem_coe, xS]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
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
rw rw₁ rw₂ rw₃ :
  ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
    ∃ (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 ⋯)
rw₄ rw₅ :
  ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
    ∃ (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 ⋯)
⊢ Language.order.IsExtensionPair M N
have rw₆ : ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
  let this := Language.order.linearOrderOfModels N;
  ∀ (this : DenselyOrdered N),
    ∃ (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 sorry)
Tactic: classical
  rw [isExtensionPair_iff_exists_embedding_closure_singleton_sup]
  intro S S_fg f m
  letI := Language.order.linearOrderOfModels M
  letI := Language.order.linearOrderOfModels N
  have := Language.order.denselyOrdered_of_dlo N
  have := Language.order.noBotOrder_of_dlo N
  have := Language.order.noTopOrder_of_dlo N
  have := NoBotOrder.to_noMinOrder N
  have := NoTopOrder.to_noMaxOrder N
  have hS : Set.Finite (S : Set M) := (S.fg_iff_structure_fg.1 S_fg).finite
  obtain ⟨g, hg⟩ := Order.exists_orderEmbedding_insert hS.toFinset
    ((OrderIso.setCongr hS.toFinset (S : Set M) hS.coe_toFinset).toOrderEmbedding.trans
      (OrderEmbedding.ofStrictMono f (HomClass.strictMono f))) m
  let g' :
    ((Substructure.closure Language.order).toFun {m} ⊔ S : Language.order.Substructure M) ↪o N :=
    ((OrderIso.setCongr _ _ (by
      convert!
        LowerAdjoint.closure_eq_self_of_mem_closed _
          (Substructure.mem_closed_of_isRelational Language.order
            ((insert m hS.toFinset : Finset M) : Set M))
      simp only [Finset.coe_insert, Set.Finite.coe_toFinset, Substructure.closure_insert,
        Substructure.closure_eq])).toOrderEmbedding.trans g)
  use StrongHomClass.toEmbedding g'
  ext ⟨x, xS⟩
  refine congr_fun hg.symm ⟨x, (?_ : x ∈ hS.toFinset)⟩
  simp only [Set.Finite.mem_toFinset, SetLike.mem_coe, xS]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
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
rw rw₁ rw₂ rw₃ :
  ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
    ∃ (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 ⋯)
rw₄ rw₅ :
  ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
    ∃ (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 ⋯)
rw₆ :
  ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
    let this := Language.order.linearOrderOfModels N;
    ∀ (this : DenselyOrdered N),
      ∃ (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 ⋯)
⊢ Language.order.IsExtensionPair M N
have rw₇ : ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
  let this := Language.order.linearOrderOfModels N;
  ∀ (this_1 : DenselyOrdered N) (this : NoBotOrder N),
    ∃ (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 sorry)
Tactic: classical
  rw [isExtensionPair_iff_exists_embedding_closure_singleton_sup]
  intro S S_fg f m
  letI := Language.order.linearOrderOfModels M
  letI := Language.order.linearOrderOfModels N
  have := Language.order.denselyOrdered_of_dlo N
  have := Language.order.noBotOrder_of_dlo N
  have := Language.order.noTopOrder_of_dlo N
  have := NoBotOrder.to_noMinOrder N
  have := NoTopOrder.to_noMaxOrder N
  have hS : Set.Finite (S : Set M) := (S.fg_iff_structure_fg.1 S_fg).finite
  obtain ⟨g, hg⟩ := Order.exists_orderEmbedding_insert hS.toFinset
    ((OrderIso.setCongr hS.toFinset (S : Set M) hS.coe_toFinset).toOrderEmbedding.trans
      (OrderEmbedding.ofStrictMono f (HomClass.strictMono f))) m
  let g' :
    ((Substructure.closure Language.order).toFun {m} ⊔ S : Language.order.Substructure M) ↪o N :=
    ((OrderIso.setCongr _ _ (by
      convert!
        LowerAdjoint.closure_eq_self_of_mem_closed _
          (Substructure.mem_closed_of_isRelational Language.order
            ((insert m hS.toFinset : Finset M) : Set M))
      simp only [Finset.coe_insert, Set.Finite.coe_toFinset, Substructure.closure_insert,
        Substructure.closure_eq])).toOrderEmbedding.trans g)
  use StrongHomClass.toEmbedding g'
  ext ⟨x, xS⟩
  refine congr_fun hg.symm ⟨x, (?_ : x ∈ hS.toFinset)⟩
  simp only [Set.Finite.mem_toFinset, SetLike.mem_coe, xS]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
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 ℚ
⊢ Infinite M
have obtain : ∀ (f : ℚ ↪[Language.order] M), (↑default : ℚ ≃ₚ[Language.order] M) ≤ f.toPartialEquiv → Infinite M
Tactic: obtain ⟨f, _⟩ := embedding_from_cg cg_of_countable default (dlo_isExtensionPair ℚ M)
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
M : Type w'
inst : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst_1 : Nonempty M
⊢ 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}
have 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
Tactic: ext N
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
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
have 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)
Tactic: refine ⟨fun ⟨hF, h⟩ => ⟨hF.finite, Theory.IsUniversal.models_of_embedding h.some⟩,
    fun ⟨hF, h⟩ => ⟨FG.of_finite, ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
M : Type w'
inst : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst_1 : Nonempty M
⊢ Language.order.age M =
    {M : CategoryTheory.Bundled Language.order.Structure |
      Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}
have rw : 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: classical
  rw [age]
  ext N
  refine ⟨fun ⟨hF, h⟩ => ⟨hF.finite, Theory.IsUniversal.models_of_embedding h.some⟩,
    fun ⟨hF, h⟩ => ⟨FG.of_finite, ?_⟩⟩
  letI := Language.order.linearOrderOfModels M
  letI := Language.order.linearOrderOfModels N
  exact ⟨StrongHomClass.toEmbedding (nonempty_orderEmbedding_of_finite_infinite N M).some⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
M : Type w'
inst : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst_1 : Nonempty M
rw rw₁ rw₂ :
  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}
⊢ Language.order.age M =
    {M : CategoryTheory.Bundled Language.order.Structure |
      Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}
have 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
Tactic: classical
  rw [age]
  ext N
  refine ⟨fun ⟨hF, h⟩ => ⟨hF.finite, Theory.IsUniversal.models_of_embedding h.some⟩,
    fun ⟨hF, h⟩ => ⟨FG.of_finite, ?_⟩⟩
  letI := Language.order.linearOrderOfModels M
  letI := Language.order.linearOrderOfModels N
  exact ⟨StrongHomClass.toEmbedding (nonempty_orderEmbedding_of_finite_infinite N M).some⟩