awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
inst_4 : Language.order.Structure M
inst_5 : Language.order.OrderedStructure M
⊢ ∀ {n : ℕ} (R : Language.order.Relations n) (x : Fin n → M), RelMap (L.orderLHom.onRelation R) x = RelMap R x

Tactic:
simp [order.relation_eq_leSymb]

Premises used: FirstOrder.Language.order.relation_eq_leSymb
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
S : L.Substructure M
⊢ OrderedStructure.{u, v, w'} L ↥S

Tactic:
⟨fun x => relMap_leSymb (S.subtype ∘ x)⟩

Premises used: FirstOrder.Language.OrderedStructure.relMap_leSymb, Function.comp, FirstOrder.Language.Substructure.subtype, FirstOrder.Language.OrderedStructure.mk, DFunLike.coe
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
t₁ t₂ : Term.{u, v, w} L (α ⊕ Fin n)
v : α → M
xs : Fin n → M
⊢ (t₁.le t₂).Realize v xs ↔ realize (Sum.elim v xs) t₁ ≤ realize (Sum.elim v xs) t₂

Tactic:
simp [Term.le]

Premises used: FirstOrder.Language.Term.le
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
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
⊢ M ⊨ L.noTopOrderSentence ↔ NoTopOrder M

Tactic:
simp only [noTopOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all,
    BoundedFormula.realize_ex, BoundedFormula.realize_not, Term.realize_le]

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.BoundedFormula.realize_ex, FirstOrder.Language.BoundedFormula.realize_not, FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.Term.realize_le, FirstOrder.Language.noTopOrderSentence, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Order
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

Tactic:
⟨fun h => ⟨fun a => h a⟩, ?_⟩

Premises used: Iff.intro, NoTopOrder.mk
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
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))
⊢ (∀ (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:
refine ⟨fun h => ⟨fun a => h a⟩, ?_⟩
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
h : 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:
exists_not_le a

Premises used: cast, Fin.snoc, dite, NoTopOrder.exists_not_le, FirstOrder.Language.Term.realize, Sum.elim
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
h : 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:
exact exists_not_le a

Premises used: NoTopOrder.exists_not_le
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
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
⊢ M ⊨ L.noBotOrderSentence ↔ NoBotOrder M

Tactic:
simp only [noBotOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all,
    BoundedFormula.realize_ex, BoundedFormula.realize_not, Term.realize_le]

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.noBotOrderSentence, FirstOrder.Language.BoundedFormula.realize_ex, FirstOrder.Language.BoundedFormula.realize_not, FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.Term.realize_le, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Order
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

Tactic:
⟨fun h => ⟨fun a => h a⟩, ?_⟩

Premises used: NoBotOrder.mk, Iff.intro
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
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))
⊢ (∀ (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:
refine ⟨fun h => ⟨fun a => h a⟩, ?_⟩
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
h : 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:
exists_not_ge a

Premises used: cast, Fin.snoc, dite, FirstOrder.Language.Term.realize, NoBotOrder.exists_not_ge, Sum.elim
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
h : 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:
exact exists_not_ge a

Premises used: NoBotOrder.exists_not_ge
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
h : NoTopOrder M
⊢ M ⊨ L.noTopOrderSentence

Tactic:
realize_noTopOrder_iff.2 h

Premises used: Iff.mpr, FirstOrder.Language.realize_noTopOrder_iff
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
h : NoBotOrder M
⊢ M ⊨ L.noBotOrderSentence

Tactic:
realize_noBotOrder_iff.2 h

Premises used: Iff.mpr, FirstOrder.Language.realize_noBotOrder_iff
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
inst_4 : M ⊨ L.dlo
⊢ L.noTopOrderSentence ∈ L.dlo

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

Premises used: true_or, FirstOrder.Language.dlo, Set.union_insert, Set.mem_insert_iff, Set.union_singleton
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : L.OrderedStructure M
inst_4 : M ⊨ L.dlo
⊢ L.noBotOrderSentence ∈ 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
M : Type w'
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : Language.order.Structure M
inst_4 : Language.order.OrderedStructure M
⊢ L.OrderedStructure M ↔ L.orderLHom.IsExpansionOn M

Tactic:
⟨fun _ => inferInstance, fun _ => inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.ModelTheory.Order
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
simp : (Std.Refl fun (x y : M) ↦ x ≤ y) ∧ IsTrans M fun (x y : M) ↦ x ≤ y
⊢ M ⊨ L.preorderTheory

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]

Premises used: FirstOrder.Language.preorderTheory, Matrix.cons_val_one, Matrix.cons_val_zero, FirstOrder.Language.Relations.realize_transitive, FirstOrder.Language.OrderedStructure.relMap_leSymb, FirstOrder.Language.Theory.model_singleton_iff, FirstOrder.Language.Theory.model_insert_iff, FirstOrder.Language.Relations.realize_reflexive
-- Module: Mathlib.ModelTheory.Order
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
⊢ (Std.Refl fun (x y : M) ↦ x ≤ y) ∧ IsTrans M fun (x y : M) ↦ x ≤ y

Tactic:
⟨inferInstance, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.ModelTheory.Order
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
⊢ (Std.Refl fun (x y : M) ↦ x ≤ y) ∧ IsTrans M fun (x y : M) ↦ x ≤ y

Tactic:
exact ⟨inferInstance, inferInstance⟩
-- Module: Mathlib.ModelTheory.Order
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
t₁ t₂ : Term.{u, v, w} L (α ⊕ Fin n)
v : α → M
xs : Fin n → M
⊢ (t₁.lt t₂).Realize v xs ↔ realize (Sum.elim v xs) t₁ < realize (Sum.elim v xs) t₂

Tactic:
simp [Term.lt, lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge, FirstOrder.Language.Term.lt
-- 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
⊢ (∀ (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:
⟨fun h => ⟨fun a b ab => h a b ab⟩, ?_⟩

Premises used: DenselyOrdered.mk, Iff.intro
-- 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
h : DenselyOrdered M
a b : M
ab :
  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)
          b))
      ((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)
          b))
      ((var ∘ Sum.inr) 1))
⊢ ∃ (a_1 : 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) b)
              a_1))
          ((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) b)
              a_1))
          ((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) b)
              a_1))
          ((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) b)
              a_1))
          ((var ∘ Sum.inr) 1))

Tactic:
exists_between ab

Premises used: cast, Fin.snoc, exists_between, dite, FirstOrder.Language.Term.realize, Sum.elim
-- 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
h : DenselyOrdered M
a b : M
ab :
  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)
          b))
      ((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)
          b))
      ((var ∘ Sum.inr) 1))
⊢ ∃ (a_1 : 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) b)
              a_1))
          ((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) b)
              a_1))
          ((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) b)
              a_1))
          ((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) b)
              a_1))
          ((var ∘ Sum.inr) 1))

Tactic:
exact exists_between ab

Premises used: exists_between
-- 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
h : DenselyOrdered M
⊢ M ⊨ L.denselyOrderedSentence

Tactic:
realize_denselyOrdered_iff.2 h

Premises used: Iff.mpr, FirstOrder.Language.realize_denselyOrdered_iff