-- Mathlib/ModelTheory/Order.lean
theorem realize_denselyOrdered_iff :
    M ⊨ L.denselyOrderedSentence ↔ DenselyOrdered M

Proof state:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
⊢ DenselyOrdered M →
    ∀ (a a_1 : M),
      Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) <
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) →
        ∃ a_3,
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 0) <
              Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) ∧
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) <
              Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 1)

Tactic:
intro h a b ab

Result:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
h : DenselyOrdered M
a b : M
ab :
  Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) b)) ((var ∘ Sum.inr) 0) <
    Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) b)) ((var ∘ Sum.inr) 1)
⊢ ∃ a_1,
    Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 0) <
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 2) ∧
      Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 2) <
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 1)

Proof state:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.denselyOrderedSentence ↔ DenselyOrdered M

Tactic:
simp only [denselyOrderedSentence, Sentence.Realize, Formula.Realize,
  BoundedFormula.realize_imp, BoundedFormula.realize_all, Term.realize, Term.realize_lt,
  Sum.elim_inr, BoundedFormula.realize_ex, BoundedFormula.realize_inf]

Result:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
⊢ (∀ (a a_1 : M),
      Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) <
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) →
        ∃ a_3,
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 0) <
              Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) ∧
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) <
              Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 1)) ↔
    DenselyOrdered M

Proof state:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
⊢ (∀ (a a_1 : M),
      Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) <
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) →
        ∃ a_3,
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 0) <
              Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) ∧
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) <
              Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 1)) ↔
    DenselyOrdered M

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

Result:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
⊢ DenselyOrdered M →
    ∀ (a a_1 : M),
      Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) <
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) →
        ∃ a_3,
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 0) <
              Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) ∧
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) <
              Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 1)

Proof state:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
h : DenselyOrdered M
a b : M
ab :
  Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) b)) ((var ∘ Sum.inr) 0) <
    Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) b)) ((var ∘ Sum.inr) 1)
⊢ ∃ a_1,
    Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 0) <
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 2) ∧
      Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 2) <
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 1)

Tactic:
exact exists_between ab

Result:
no goals