[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ OrderedStructure Language.order M
[PROOFSTEP]
rw [orderedStructure_iff, orderLHom_order]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ LHom.IsExpansionOn (LHom.id Language.order) M
[PROOFSTEP]
exact LHom.id_isExpansionOn M
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ M ⊨ preorderTheory Language.order
[PROOFSTEP]
simp only [preorderTheory, Theory.model_iff, Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp,
  Relations.realize_reflexive, relMap_apply₂, forall_eq, Relations.realize_transitive]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ (Reflexive fun x y => x ≤ y) ∧ Transitive fun x y => x ≤ y
[PROOFSTEP]
exact ⟨le_refl, fun _ _ _ => le_trans⟩
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : PartialOrder M
⊢ M ⊨ partialOrderTheory Language.order
[PROOFSTEP]
simp only [partialOrderTheory, Theory.model_iff, Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp,
  Relations.realize_reflexive, relMap_apply₂, Relations.realize_antisymmetric, forall_eq, Relations.realize_transitive]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : PartialOrder M
⊢ (Reflexive fun x y => x ≤ y) ∧ (AntiSymmetric fun x y => x ≤ y) ∧ Transitive fun x y => x ≤ y
[PROOFSTEP]
exact ⟨le_refl, fun _ _ => le_antisymm, fun _ _ _ => le_trans⟩
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LinearOrder M
⊢ M ⊨ linearOrderTheory Language.order
[PROOFSTEP]
simp only [linearOrderTheory, Theory.model_iff, Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp,
  Relations.realize_reflexive, relMap_apply₂, Relations.realize_antisymmetric, Relations.realize_transitive, forall_eq,
  Relations.realize_total]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LinearOrder M
⊢ (Reflexive fun x y => x ≤ y) ∧
    (AntiSymmetric fun x y => x ≤ y) ∧ (Transitive fun x y => x ≤ y) ∧ Total fun x y => x ≤ y
[PROOFSTEP]
exact ⟨le_refl, fun _ _ => le_antisymm, fun _ _ _ => le_trans, le_total⟩
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : IsOrdered L
inst✝² : Structure L M
inst✝¹ : LE M
inst✝ : OrderedStructure L M
a b : M
⊢ RelMap leSymb ![a, b] ↔ a ≤ b
[PROOFSTEP]
rw [← orderLHom_leSymb, LHom.map_onRelation]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : IsOrdered L
inst✝² : Structure L M
inst✝¹ : LE M
inst✝ : OrderedStructure L M
a b : M
⊢ RelMap leSymb ![a, b] ↔ a ≤ b
[PROOFSTEP]
rfl
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : IsOrdered L
inst✝² : Structure L M
inst✝¹ : LE M
inst✝ : OrderedStructure L M
t₁ t₂ : Term L (α ⊕ Fin n)
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize (le t₁ t₂) v xs ↔ realize (Sum.elim v xs) t₁ ≤ realize (Sum.elim v xs) t₂
[PROOFSTEP]
simp [Term.le]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : IsOrdered L
inst✝² : Structure L M
inst✝¹ : Preorder M
inst✝ : OrderedStructure L M
t₁ t₂ : Term L (α ⊕ Fin n)
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize (lt t₁ t₂) v xs ↔ realize (Sum.elim v xs) t₁ < realize (Sum.elim v xs) t₂
[PROOFSTEP]
simp [Term.lt, lt_iff_le_not_le]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ M ⊨ noTopOrderSentence Language.order ↔ NoTopOrder M
[PROOFSTEP]
simp only [noTopOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all, BoundedFormula.realize_ex,
  BoundedFormula.realize_not, Term.realize, Term.realize_le, Sum.elim_inr]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ (∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0) ↔ NoTopOrder M
[PROOFSTEP]
refine' ⟨fun h => ⟨fun a => h a⟩, _⟩
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ NoTopOrder M → ∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0
[PROOFSTEP]
intro h a
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
h : NoTopOrder M
a : M
⊢ ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0
[PROOFSTEP]
exact exists_not_le a
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ M ⊨ noBotOrderSentence Language.order ↔ NoBotOrder M
[PROOFSTEP]
simp only [noBotOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all, BoundedFormula.realize_ex,
  BoundedFormula.realize_not, Term.realize, Term.realize_le, Sum.elim_inr]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ (∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 0 ≤ Fin.snoc (Fin.snoc default a) a_1 1) ↔ NoBotOrder M
[PROOFSTEP]
refine' ⟨fun h => ⟨fun a => h a⟩, _⟩
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
⊢ NoBotOrder M → ∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 0 ≤ Fin.snoc (Fin.snoc default a) a_1 1
[PROOFSTEP]
intro h a
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : LE M
h : NoBotOrder M
a : M
⊢ ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 0 ≤ Fin.snoc (Fin.snoc default a) a_1 1
[PROOFSTEP]
exact exists_not_ge a
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : Preorder M
⊢ M ⊨ denselyOrderedSentence Language.order ↔ DenselyOrdered M
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]
refine' ⟨fun h => ⟨fun a b ab => h a b ab⟩, _⟩
[GOAL]
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
[PROOFSTEP]
intro h a b ab
[GOAL]
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
[PROOFSTEP]
exact exists_between ab
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
inst✝¹ : NoTopOrder M
inst✝ : NoBotOrder M
⊢ M ⊨ dlo Language.order
[PROOFSTEP]
simp only [dlo, Set.union_insert, Set.union_singleton, Theory.model_iff, Set.mem_insert_iff, forall_eq_or_imp,
  realize_noTopOrder, realize_noBotOrder, realize_denselyOrdered, true_and_iff]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
inst✝¹ : NoTopOrder M
inst✝ : NoBotOrder M
⊢ ∀ (a : Sentence Language.order), a ∈ linearOrderTheory Language.order → M ⊨ a
[PROOFSTEP]
rw [← Theory.model_iff]
[GOAL]
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
inst✝¹ : NoTopOrder M
inst✝ : NoBotOrder M
⊢ M ⊨ linearOrderTheory Language.order
[PROOFSTEP]
infer_instance
