awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : Preorder M
inst_3 : L.OrderedStructure M
inst_4 : M ⊨ L.dlo
⊢ L.denselyOrderedSentence ∈ L.dlo

Tactic:
simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or, or_true]

Premises used: true_or, FirstOrder.Language.dlo, Set.union_insert, Set.mem_insert_iff, or_true, Set.union_singleton
-- Module: Mathlib.ModelTheory.Order
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
simp : Std.Antisymm fun (x y : M) ↦ x ≤ y
⊢ M ⊨ L.partialOrderTheory

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]

Premises used: FirstOrder.Language.partialOrderTheory, and_true, FirstOrder.Language.model_preorder, Matrix.cons_val_one, Matrix.cons_val_zero, FirstOrder.Language.OrderedStructure.relMap_leSymb, FirstOrder.Language.Theory.model_insert_iff, Fin.isValue, FirstOrder.Language.Relations.realize_antisymmetric
-- Module: Mathlib.ModelTheory.Order
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
⊢ Std.Antisymm fun (x y : M) ↦ x ≤ y

Tactic:
infer_instance
-- Module: Mathlib.ModelTheory.Order
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
simp : Std.Total fun (x y : M) ↦ x ≤ y
⊢ M ⊨ L.linearOrderTheory

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]

Premises used: and_true, FirstOrder.Language.model_partialOrder, Matrix.cons_val_one, Matrix.cons_val_zero, FirstOrder.Language.OrderedStructure.relMap_leSymb, FirstOrder.Language.Relations.realize_total, FirstOrder.Language.Theory.model_insert_iff, FirstOrder.Language.linearOrderTheory, Fin.isValue
-- Module: Mathlib.ModelTheory.Order
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
⊢ Std.Total fun (x y : M) ↦ x ≤ y

Tactic:
infer_instance
-- Module: Mathlib.ModelTheory.Order
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
inst_4 : DenselyOrdered M
inst_5 : NoTopOrder M
inst_6 : NoBotOrder M
⊢ M ⊨ L.dlo

Tactic:
simp [dlo, model_linearOrder, Theory.model_insert_iff]

Premises used: FirstOrder.Language.dlo, FirstOrder.Language.model_linearOrder, FirstOrder.Language.Theory.model_insert_iff
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
this : LE M := L.leOfStructure M
relMap_leSymb : ∀ (x : Fin 2 → M), RelMap.{u, v, w'} (L := L) leSymb x ↔ x 0 ≤ x 1
⊢ L.OrderedStructure M

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
this : LE M := L.leOfStructure M
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
⊢ ∀ (x : Fin 2 → M), RelMap.{u, v, w'} (L := L) leSymb x ↔ x 0 ≤ x 1

Tactic:
simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]

Premises used: Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi, Fin.cons_zero
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
this : LE M := L.leOfStructure M
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:
rfl
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
h : M ⊨ L.preorderTheory
⊢ Relations.reflexive leSymb ∈ L.preorderTheory

Tactic:
simp [preorderTheory]

Premises used: FirstOrder.Language.preorderTheory
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
h : M ⊨ L.preorderTheory
⊢ Relations.transitive leSymb ∈ L.preorderTheory

Tactic:
simp [preorderTheory]

Premises used: FirstOrder.Language.preorderTheory
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
h : M ⊨ L.partialOrderTheory
⊢ Relations.antisymmetric leSymb ∈ L.partialOrderTheory

Tactic:
simp [partialOrderTheory]

Premises used: FirstOrder.Language.partialOrderTheory
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
h : M ⊨ L.linearOrderTheory
inst_2 : DecidableRel fun (a b : M) ↦ RelMap.{u, v, w'} (L := L) leSymb ![a, b]
⊢ Relations.total leSymb ∈ L.linearOrderTheory

Tactic:
simp [linearOrderTheory]

Premises used: FirstOrder.Language.linearOrderTheory
-- Module: Mathlib.ModelTheory.Order
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
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)
⊢ ∀ (φ : 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)

Tactic:
simp only [forall_relations, relation_eq_leSymb, relMap_leSymb, Fin.isValue,
      Function.comp_apply]

Premises used: FirstOrder.Language.order.forall_relations, FirstOrder.Language.order.relation_eq_leSymb, FirstOrder.Language.OrderedStructure.relMap_leSymb, Fin.isValue, Function.comp_apply
-- Module: Mathlib.ModelTheory.Order
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) (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:
fun φ x => map_rel φ

Premises used: RelHomClass.map_rel
-- Module: Mathlib.ModelTheory.Order
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) (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:
exact fun φ x => map_rel φ

Premises used: RelHomClass.map_rel
-- Module: Mathlib.ModelTheory.Order
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
⊢ ∀ (φ : M ↪o N) {n : ℕ} (r : Language.order.Relations n) (x : Fin n → M),
    RelMap.{0, 0, u_1} (M := N) r ((⇑φ : (a : M) → N) ∘ x) ↔ RelMap r x

Tactic:
simp only [order.forall_relations, order.relation_eq_leSymb, relMap_leSymb, Fin.isValue,
    Function.comp_apply, RelEmbedding.map_rel_iff, implies_true]

Premises used: FirstOrder.Language.order.forall_relations, FirstOrder.Language.order.relation_eq_leSymb, FirstOrder.Language.OrderedStructure.relMap_leSymb, RelEmbedding.map_rel_iff, Fin.isValue, Function.comp_apply, implies_true
-- Module: Mathlib.ModelTheory.Order
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 : EquivLike F M N
inst_7 : OrderIsoClass F M N
⊢ ∀ (φ : F) {n : ℕ} (r : Language.order.Relations n) (x : Fin n → M),
    RelMap.{0, 0, u_1} (M := N) r ((⇑φ : (a : M) → N) ∘ x) ↔ RelMap r x

Tactic:
simp only [order.forall_relations, order.relation_eq_leSymb, relMap_leSymb, Fin.isValue,
      Function.comp_apply, map_le_map_iff, implies_true]

Premises used: OrderIsoClass.map_le_map_iff, FirstOrder.Language.order.forall_relations, FirstOrder.Language.order.relation_eq_leSymb, FirstOrder.Language.OrderedStructure.relMap_leSymb, Fin.isValue, Function.comp_apply, implies_true
-- Module: Mathlib.ModelTheory.Order
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
⊢ 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]
-- Module: Mathlib.ModelTheory.Order
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
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])
⊢ a ≤ b → LE.le.{u_1} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)

Tactic:
simp only [relMap_leSymb, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
    Function.comp_apply] at h

Premises used: Matrix.cons_val_one, Matrix.cons_val_zero, FirstOrder.Language.OrderedStructure.relMap_leSymb, Fin.isValue, Function.comp_apply
-- Module: Mathlib.ModelTheory.Order
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
h : a ≤ b → LE.le.{u_1} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)
⊢ a ≤ b → LE.le.{u_1} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)

Tactic:
h
-- Module: Mathlib.ModelTheory.Order
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
h : a ≤ b → LE.le.{u_1} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)
⊢ a ≤ b → LE.le.{u_1} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)

Tactic:
exact h
-- Module: Mathlib.ModelTheory.Order
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 : EmbeddingLike F M N
inst_6 : PartialOrder M
inst_7 : L.OrderedStructure M
inst_8 : PartialOrder N
inst_9 : L.OrderedStructure N
f : F
⊢ StrictMono.{w', u_1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
(HomClass.monotone f).strictMono_of_injective (EmbeddingLike.injective f)

Premises used: FirstOrder.Language.HomClass.monotone, EmbeddingLike.injective, Monotone.strictMono_of_injective
-- Module: Mathlib.ModelTheory.Order
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
⊢ 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]
-- Module: Mathlib.ModelTheory.Order
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
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]
⊢ LE.le.{u_2} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ↔ a ≤ b

Tactic:
simp only [relMap_leSymb, Fin.isValue, Function.comp_apply, Matrix.cons_val_zero,
      Matrix.cons_val_one] at h

Premises used: Matrix.cons_val_one, Matrix.cons_val_zero, FirstOrder.Language.OrderedStructure.relMap_leSymb, Fin.isValue, Function.comp_apply
-- Module: Mathlib.ModelTheory.Order
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
h : LE.le.{u_2} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ↔ a ≤ b
⊢ LE.le.{u_2} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ↔ a ≤ b

Tactic:
h
-- Module: Mathlib.ModelTheory.Order
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
h : LE.le.{u_2} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ↔ a ≤ b
⊢ LE.le.{u_2} (α := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ↔ a ≤ b

Tactic:
exact h
-- 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
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 ⋯)
⊢ Language.order.IsExtensionPair M N

Tactic:
rw [isExtensionPair_iff_exists_embedding_closure_singleton_sup]

Premises used: FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup
-- 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 : LinearOrder N := Language.order.linearOrderOfModels N
⊢ DenselyOrdered N

Tactic:
have := Language.order.denselyOrdered_of_dlo N
-- 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 : DenselyOrdered N
⊢ NoBotOrder N

Tactic:
have := Language.order.noBotOrder_of_dlo N
-- 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 : NoBotOrder N
⊢ NoTopOrder N

Tactic:
have := Language.order.noTopOrder_of_dlo N
-- 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 : NoTopOrder N
⊢ NoMinOrder N

Tactic:
have := NoBotOrder.to_noMinOrder N
-- 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 : NoMinOrder N
⊢ NoMaxOrder N

Tactic:
have := NoTopOrder.to_noMaxOrder N
-- 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
⊢ (↑S : Set M).Finite

Tactic:
have hS : Set.Finite (S : Set M) := (S.fg_iff_structure_fg.1 S_fg).finite
-- 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
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)) ⋯))
        (⇑(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 :
      Embedding.{0, 0, w, w'} Language.order
        (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S)) N),
      f = g.comp (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:
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

Premises used: Order.exists_orderEmbedding_insert, Set.Finite.toFinset
-- 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)
          (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)) :
      Set M) =
    (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)

Tactic:
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