-- 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
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
⊢ M ⊨ L.denselyOrderedSentence ↔ 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]

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.BoundedFormula.realize_inf, FirstOrder.Language.BoundedFormula.realize_ex, FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.Term.realize_lt, FirstOrder.Language.denselyOrderedSentence, FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.Formula.Realize