awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
⊢ ∀ ⦃φ : L.Sentence⦄, φ ∈ L.preorderTheory → BoundedFormula.IsUniversal φ
have simp : BoundedFormula.IsUniversal.{u, v, 0} (L := L) (Relations.reflexive leSymb) ∧
  BoundedFormula.IsUniversal.{u, v, 0} (L := L) (Relations.transitive leSymb)
Tactic: simp only [preorderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp, forall_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : Language.order.Structure M
inst_4 : Language.order.OrderedStructure M
inst_5 : L.orderLHom.IsExpansionOn M
x : Fin 2 → M
⊢ RelMap.{u, v, w'} (L := L) leSymb x ↔ x 0 ≤ x 1
have rw : RelMap (L.orderLHom.onRelation leSymb) x ↔ x 0 ≤ x 1
Tactic: rw [← orderLHom_leSymb L, LHom.IsExpansionOn.map_onRelation, relMap_leSymb]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : Language.order.Structure M
inst_4 : Language.order.OrderedStructure M
inst_5 : L.orderLHom.IsExpansionOn M
x : Fin 2 → M
rw : RelMap (L.orderLHom.onRelation leSymb) x ↔ x 0 ≤ x 1
⊢ RelMap.{u, v, w'} (L := L) leSymb x ↔ x 0 ≤ x 1
have rw₁ : RelMap (L := Language.order) leSymb x ↔ x 0 ≤ x 1
Tactic: rw [← orderLHom_leSymb L, LHom.IsExpansionOn.map_onRelation, relMap_leSymb]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : Language.order.Structure M
inst_4 : Language.order.OrderedStructure M
inst_5 : L.orderLHom.IsExpansionOn M
x : Fin 2 → M
rw : RelMap (L.orderLHom.onRelation leSymb) x ↔ x 0 ≤ x 1
rw₁ : RelMap (L := Language.order) leSymb x ↔ x 0 ≤ x 1
⊢ RelMap.{u, v, w'} (L := L) leSymb x ↔ x 0 ≤ x 1
have rw₂ : x 0 ≤ x 1 ↔ x 0 ≤ x 1
Tactic: rw [← orderLHom_leSymb L, LHom.IsExpansionOn.map_onRelation, relMap_leSymb]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
⊢ M ⊨ L.noTopOrderSentence ↔ NoTopOrder M
have simp : (∀ (a : M),
    ∃ (a_1 : M),
      ¬LE.le.{w'} (α := M)
          (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
            (Sum.elim default
              (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
            ((var ∘ Sum.inr) 1))
          (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
            (Sum.elim default
              (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
            ((var ∘ Sum.inr) 0))) ↔
  NoTopOrder M
Tactic: simp only [noTopOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all,
    BoundedFormula.realize_ex, BoundedFormula.realize_not, Term.realize_le]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
⊢ (∀ (a : M),
      ∃ (a_1 : M),
        ¬LE.le.{w'} (α := M)
            (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
              (Sum.elim default
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                  (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
              ((var ∘ Sum.inr) 1))
            (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
              (Sum.elim default
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                  (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
              ((var ∘ Sum.inr) 0))) ↔
    NoTopOrder M
have refine : NoTopOrder M →
  ∀ (a : M),
    ∃ (a_1 : M),
      ¬LE.le.{w'} (α := M)
          (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
            (Sum.elim default
              (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
            ((var ∘ Sum.inr) 1))
          (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
            (Sum.elim default
              (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
            ((var ∘ Sum.inr) 0))
Tactic: refine ⟨fun h => ⟨fun a => h a⟩, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
⊢ M ⊨ L.noBotOrderSentence ↔ NoBotOrder M
have simp : (∀ (a : M),
    ∃ (a_1 : M),
      ¬LE.le.{w'} (α := M)
          (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
            (Sum.elim default
              (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
            ((var ∘ Sum.inr) 0))
          (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
            (Sum.elim default
              (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
            ((var ∘ Sum.inr) 1))) ↔
  NoBotOrder M
Tactic: simp only [noBotOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all,
    BoundedFormula.realize_ex, BoundedFormula.realize_not, Term.realize_le]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
⊢ (∀ (a : M),
      ∃ (a_1 : M),
        ¬LE.le.{w'} (α := M)
            (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
              (Sum.elim default
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                  (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
              ((var ∘ Sum.inr) 0))
            (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
              (Sum.elim default
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                  (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
              ((var ∘ Sum.inr) 1))) ↔
    NoBotOrder M
have refine : NoBotOrder M →
  ∀ (a : M),
    ∃ (a_1 : M),
      ¬LE.le.{w'} (α := M)
          (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
            (Sum.elim default
              (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
            ((var ∘ Sum.inr) 0))
          (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
            (Sum.elim default
              (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
            ((var ∘ Sum.inr) 1))
Tactic: refine ⟨fun h => ⟨fun a => h a⟩, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : Preorder M
inst_3 : L.OrderedStructure M
⊢ M ⊨ L.preorderTheory
have simp : (Std.Refl fun (x y : M) ↦ x ≤ y) ∧ IsTrans M fun (x y : M) ↦ x ≤ y
Tactic: simp only [preorderTheory, Theory.model_insert_iff, Relations.realize_reflexive, relMap_leSymb,
    Theory.model_singleton_iff, Relations.realize_transitive, Matrix.cons_val_zero,
    Matrix.cons_val_one]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : Preorder M
inst_3 : L.OrderedStructure M
⊢ M ⊨ L.denselyOrderedSentence ↔ DenselyOrdered M
have simp : (∀ (a a_1 : M),
    LT.lt.{w'} (α := M)
        (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
          (Sum.elim default
            (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
              (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
          ((var ∘ Sum.inr) 0))
        (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ)
          (Sum.elim default
            (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
              (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1))
          ((var ∘ Sum.inr) 1)) →
      ∃ (a_3 : M),
        LT.lt.{w'} (α := M)
            (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ.succ)
              (Sum.elim default
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ.succ) ↦ M)
                  (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                    (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1)
                  a_3))
              ((var ∘ Sum.inr) 0))
            (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ.succ)
              (Sum.elim default
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ.succ) ↦ M)
                  (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                    (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1)
                  a_3))
              ((var ∘ Sum.inr) 2)) ∧
          LT.lt.{w'} (α := M)
            (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ.succ)
              (Sum.elim default
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ.succ) ↦ M)
                  (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                    (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1)
                  a_3))
              ((var ∘ Sum.inr) 2))
            (Term.realize.{u, v, w', 0} (L := L) (α := Empty ⊕ Fin (Nat.succ 0).succ.succ)
              (Sum.elim default
                (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ.succ) ↦ M)
                  (Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M)
                    (Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) a_1)
                  a_3))
              ((var ∘ Sum.inr) 1))) ↔
  DenselyOrdered M
Tactic: simp only [denselyOrderedSentence, Sentence.Realize, Formula.Realize,
    BoundedFormula.realize_imp, BoundedFormula.realize_all, Term.realize_lt,
    BoundedFormula.realize_ex, BoundedFormula.realize_inf]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : PartialOrder M
inst_3 : L.OrderedStructure M
⊢ M ⊨ L.partialOrderTheory
have simp : Std.Antisymm fun (x y : M) ↦ x ≤ y
Tactic: simp only [partialOrderTheory, Theory.model_insert_iff, Relations.realize_antisymmetric,
    relMap_leSymb, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
    model_preorder, and_true]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LinearOrder M
inst_3 : L.OrderedStructure M
⊢ M ⊨ L.linearOrderTheory
have simp : Std.Total fun (x y : M) ↦ x ≤ y
Tactic: simp only [linearOrderTheory, Theory.model_insert_iff, Relations.realize_total, relMap_leSymb,
    Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, model_partialOrder,
    and_true]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
this : LE M := L.leOfStructure M
⊢ L.OrderedStructure M
have relMap_leSymb : ∀ (x : Fin 2 → M), RelMap.{u, v, w'} (L := L) leSymb x ↔ x 0 ≤ x 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
this : LE M := L.leOfStructure M
⊢ ∀ (x : Fin 2 → M), RelMap.{u, v, w'} (L := L) leSymb x ↔ x 0 ≤ x 1
have relMap_leSymb : ∀ (a a_1 : M),
  RelMap.{u, v, w'} (L := L) (M := M) leSymb
      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ M) a
        (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ M) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ M)))) ↔
    a ≤
      Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ M) a
        (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ M) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ M))) 1
Tactic: simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : Language.order.Structure M
inst_1 : LE M
inst_2 : Language.order.OrderedStructure M
N : Type u_1
inst_3 : Language.order.Structure N
inst_4 : LE N
inst_5 : Language.order.OrderedStructure N
F : Type u_2
inst_6 : FunLike F M N
inst_7 : OrderHomClass F M N
⊢ ∀ (φ : F) {n : ℕ} (r : Language.order.Relations n) (x : Fin n → M),
    RelMap r x → RelMap.{0, 0, u_1} (M := N) r ((⇑φ : (a : M) → N) ∘ x)
have simp : ∀ (φ : F) (x : Fin 2 → M), x 0 ≤ x 1 → LE.le.{u_1} (α := N) ((φ : (a : M) → N) (x 0) : N) ((φ : (a : M) → N) (x 1) : N)
Tactic: simp only [forall_relations, relation_eq_leSymb, relMap_leSymb, Fin.isValue,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (hypothesis)
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
N : Type u_1
inst_2 : L.Structure N
F : Type u_2
inst_3 : FunLike F M N
inst_4 : L.HomClass F M N
inst_5 : Preorder M
inst_6 : L.OrderedStructure M
inst_7 : Preorder N
inst_8 : L.OrderedStructure N
f : F
a b : M
⊢ a ≤ b → LE.le.{u_1} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)
have h : RelMap.{u, v, w'} (L := L) leSymb ![a, b] → RelMap.{u, v, u_1} (L := L) (M := N) leSymb ((⇑f : (a : M) → N) ∘ ![a, b])
Tactic: have h := HomClass.map_rel f leSymb ![a, b]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (hypothesis)
Goal:
L : Language
inst : L.IsOrdered
M : Type u_1
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
N : Type u_2
inst_4 : L.Structure N
inst_5 : LE N
inst_6 : L.OrderedStructure N
F : Type u_3
inst_7 : EquivLike F M N
inst_8 : L.StrongHomClass F M N
f : F
a b : M
⊢ LE.le.{u_2} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ↔ a ≤ b
have h : RelMap.{u_4, u_5, u_2} (L := L) (M := N) leSymb ((⇑f : (a : M) → N) ∘ ![a, b]) ↔
  RelMap.{u_4, u_5, u_1} (L := L) leSymb ![a, b]
Tactic: have h := StrongHomClass.map_rel f leSymb ![a, b]
-- 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: rw [isExtensionPair_iff_exists_embedding_closure_singleton_sup]
-- Lean 4 proof step from Mathlib.ModelTheory.Order (hypothesis)
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 : LinearOrder N := Language.order.linearOrderOfModels 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 ⋯)
have this₁ : DenselyOrdered N
Tactic: have := Language.order.denselyOrdered_of_dlo N
-- Lean 4 proof step from Mathlib.ModelTheory.Order (hypothesis)
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 : 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 ⋯)
have this₁ : NoBotOrder N
Tactic: have := Language.order.noBotOrder_of_dlo N
-- Lean 4 proof step from Mathlib.ModelTheory.Order (hypothesis)
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 : 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 ⋯)
have this₁ : NoTopOrder N
Tactic: have := Language.order.noTopOrder_of_dlo N
-- Lean 4 proof step from Mathlib.ModelTheory.Order (hypothesis)
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 : NoTopOrder 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 ⋯)
have this₁ : NoMinOrder N
Tactic: have := NoBotOrder.to_noMinOrder N
-- Lean 4 proof step from Mathlib.ModelTheory.Order (hypothesis)
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 : NoMinOrder 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 ⋯)
have this₁ : NoMaxOrder N
Tactic: have := NoTopOrder.to_noMaxOrder N
-- Lean 4 proof step from Mathlib.ModelTheory.Order (hypothesis)
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
⊢ ∃ (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 hS : (↑S : Set M).Finite
Tactic: have hS : Set.Finite (S : Set M) := (S.fg_iff_structure_fg.1 S_fg).finite
-- 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 :
    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 obtain : ∀ (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)) sorry))
      (⇑(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) sorry))
            (OrderEmbedding.ofStrictMono (⇑f : (a : ↥S) → N) sorry)) :
        (a : ↥hS.toFinset) → 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: 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