L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ (∀ (a a_1 : M),
      Fin.snoc (Fin.snoc default a) a_1 0 < Fin.snoc (Fin.snoc default a) a_1 1 →
        ∃ a_3,
          Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 0 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 ∧
            Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 1) ↔
    DenselyOrdered M
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ M ⊨ denselyOrderedSentence Language.order ↔ DenselyOrdered M
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]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ DenselyOrdered M →
    ∀ (a a_1 : M),
      Fin.snoc (Fin.snoc default a) a_1 0 < Fin.snoc (Fin.snoc default a) a_1 1 →
        ∃ a_3,
          Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 0 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 ∧
            Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 1
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ (∀ (a a_1 : M),
      Fin.snoc (Fin.snoc default a) a_1 0 < Fin.snoc (Fin.snoc default a) a_1 1 →
        ∃ a_3,
          Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 0 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 ∧
            Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 1) ↔
    DenselyOrdered M
refine' ⟨fun h => ⟨fun a b ab => h a b ab⟩, _⟩
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
h : DenselyOrdered M
a b : M
ab : Fin.snoc (Fin.snoc default a) b 0 < Fin.snoc (Fin.snoc default a) b 1
⊢ ∃ a_1,
    Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 0 < Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 2 ∧
      Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 2 < Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 1
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ DenselyOrdered M →
    ∀ (a a_1 : M),
      Fin.snoc (Fin.snoc default a) a_1 0 < Fin.snoc (Fin.snoc default a) a_1 1 →
        ∃ a_3,
          Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 0 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 ∧
            Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 1
intro h a b ab
no goals
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
h : DenselyOrdered M
a b : M
ab : Fin.snoc (Fin.snoc default a) b 0 < Fin.snoc (Fin.snoc default a) b 1
⊢ ∃ a_1,
    Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 0 < Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 2 ∧
      Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 2 < Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 1
exact exists_between ab