-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
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
have refine : DenselyOrdered 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))
Tactic: refine ⟨fun h => ⟨fun a b ab => h a b ab⟩, ?_⟩