Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded (Logic/FirstOrder/Arith/Nonstandard.lean)

State before:
c : ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
letI : Structure Language.unit ℕ := modelStar c
State after:
c : ℕ
this : Structure Language.unit ℕ := modelStar c
⊢ Satisfiable (trueArithWithStarUnbounded c)

State before:
c : ℕ
this : Structure Language.unit ℕ := modelStar c
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
haveI : Structure.Zero ℒₒᵣ⋆ ℕ := ⟨rfl⟩
State after:
c : ℕ
this✝ : Structure Language.unit ℕ := modelStar c
this : Structure.Zero ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)

State before:
c : ℕ
this✝ : Structure Language.unit ℕ := modelStar c
this : Structure.Zero ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
haveI : Structure.One ℒₒᵣ⋆ ℕ := ⟨rfl⟩
State after:
c : ℕ
this✝¹ : Structure Language.unit ℕ := modelStar c
this✝ : Structure.Zero ℒₒᵣ⋆ ℕ
this : Structure.One ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)

State before:
c : ℕ
this✝¹ : Structure Language.unit ℕ := modelStar c
this✝ : Structure.Zero ℒₒᵣ⋆ ℕ
this : Structure.One ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
haveI : Structure.Add ℒₒᵣ⋆ ℕ := ⟨fun _ _ => rfl⟩
State after:
c : ℕ
this✝² : Structure Language.unit ℕ := modelStar c
this✝¹ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝ : Structure.One ℒₒᵣ⋆ ℕ
this : Structure.Add ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)

State before:
c : ℕ
this✝² : Structure Language.unit ℕ := modelStar c
this✝¹ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝ : Structure.One ℒₒᵣ⋆ ℕ
this : Structure.Add ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
haveI : Structure.Eq ℒₒᵣ⋆ ℕ := ⟨fun _ _ => iff_of_eq rfl⟩
State after:
c : ℕ
this✝³ : Structure Language.unit ℕ := modelStar c
this✝² : Structure.Zero ℒₒᵣ⋆ ℕ
this✝¹ : Structure.One ℒₒᵣ⋆ ℕ
this✝ : Structure.Add ℒₒᵣ⋆ ℕ
this : Structure.Eq ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)

State before:
c : ℕ
this✝³ : Structure Language.unit ℕ := modelStar c
this✝² : Structure.Zero ℒₒᵣ⋆ ℕ
this✝¹ : Structure.One ℒₒᵣ⋆ ℕ
this✝ : Structure.Add ℒₒᵣ⋆ ℕ
this : Structure.Eq ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
haveI : Structure.LT ℒₒᵣ⋆ ℕ := ⟨fun _ _ => iff_of_eq rfl⟩
State after:
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)

State before:
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
have : ℕ ⊧ₘ* starUnbounded c := by
  simp [starUnbounded, models_iff]; exact Fin.prop
State after:
c : ℕ
this✝⁵ : Structure Language.unit ℕ := modelStar c
this✝⁴ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝³ : Structure.One ℒₒᵣ⋆ ℕ
this✝² : Structure.Add ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Eq ℒₒᵣ⋆ ℕ
this✝ : Structure.LT ℒₒᵣ⋆ ℕ
this : ℕ ⊧ₘ* starUnbounded c
⊢ Satisfiable (trueArithWithStarUnbounded c)

State before:
c : ℕ
this✝⁵ : Structure Language.unit ℕ := modelStar c
this✝⁴ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝³ : Structure.One ℒₒᵣ⋆ ℕ
this✝² : Structure.Add ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Eq ℒₒᵣ⋆ ℕ
this✝ : Structure.LT ℒₒᵣ⋆ ℕ
this : ℕ ⊧ₘ* starUnbounded c
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
have : ℕ ⊧ₘ* trueArithWithStarUnbounded c := by
  simp[trueArithWithStarUnbounded, models_iff]; exact this
State after:
c : ℕ
this✝⁶ : Structure Language.unit ℕ := modelStar c
this✝⁵ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝⁴ : Structure.One ℒₒᵣ⋆ ℕ
this✝³ : Structure.Add ℒₒᵣ⋆ ℕ
this✝² : Structure.Eq ℒₒᵣ⋆ ℕ
this✝¹ : Structure.LT ℒₒᵣ⋆ ℕ
this✝ : ℕ ⊧ₘ* starUnbounded c
this : ℕ ⊧ₘ* trueArithWithStarUnbounded c
⊢ Satisfiable (trueArithWithStarUnbounded c)

State before:
c : ℕ
this✝⁶ : Structure Language.unit ℕ := modelStar c
this✝⁵ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝⁴ : Structure.One ℒₒᵣ⋆ ℕ
this✝³ : Structure.Add ℒₒᵣ⋆ ℕ
this✝² : Structure.Eq ℒₒᵣ⋆ ℕ
this✝¹ : Structure.LT ℒₒᵣ⋆ ℕ
this✝ : ℕ ⊧ₘ* starUnbounded c
this : ℕ ⊧ₘ* trueArithWithStarUnbounded c
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
exact satisfiable_intro ℕ this
State after:
no goals

State before:
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ ℕ ⊧ₘ* starUnbounded c
Tactic:
simp [starUnbounded, models_iff]
State after:
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ ∀ (i : Fin c), ↑i < Semiterm.Operator.val Semiterm.Operator.Star.star ![]

State before:
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ ∀ (i : Fin c), ↑i < Semiterm.Operator.val Semiterm.Operator.Star.star ![]
Tactic:
exact Fin.prop
State after:
no goals

State before:
c : ℕ
this✝⁵ : Structure Language.unit ℕ := modelStar c
this✝⁴ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝³ : Structure.One ℒₒᵣ⋆ ℕ
this✝² : Structure.Add ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Eq ℒₒᵣ⋆ ℕ
this✝ : Structure.LT ℒₒᵣ⋆ ℕ
this : ℕ ⊧ₘ* starUnbounded c
⊢ ℕ ⊧ₘ* trueArithWithStarUnbounded c
Tactic:
simp[trueArithWithStarUnbounded, models_iff]
State after:
c : ℕ
this✝⁵ : Structure Language.unit ℕ := modelStar c
this✝⁴ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝³ : Structure.One ℒₒᵣ⋆ ℕ
this✝² : Structure.Add ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Eq ℒₒᵣ⋆ ℕ
this✝ : Structure.LT ℒₒᵣ⋆ ℕ
this : ℕ ⊧ₘ* starUnbounded c
⊢ (Structure.add ℒₒᵣ Language.unit ℕ).toStruc ⊧* starUnbounded c

State before:
c : ℕ
this✝⁵ : Structure Language.unit ℕ := modelStar c
this✝⁴ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝³ : Structure.One ℒₒᵣ⋆ ℕ
this✝² : Structure.Add ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Eq ℒₒᵣ⋆ ℕ
this✝ : Structure.LT ℒₒᵣ⋆ ℕ
this : ℕ ⊧ₘ* starUnbounded c
⊢ (Structure.add ℒₒᵣ Language.unit ℕ).toStruc ⊧* starUnbounded c
Tactic:
exact this
State after:
no goals