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

State before:
n : ℕ
⊢ ↑n < ⋆
Tactic:
have : ℕ⋆ ⊧ₘ (“!!(Semiterm.Operator.numeral ℒₒᵣ⋆ n) < ⋆” : Sentence ℒₒᵣ⋆) :=
  models_union_trueArithWithStarUnbounded.realize
    (Set.mem_iUnion_of_mem (n + 1) (Set.mem_union_right _ $ Set.mem_range_self $ Fin.last n))
State after:
n : ℕ
this :
  ℕ⋆ ⊧ₘ
    (“!!(Semiterm.Operator.const (Semiterm.Operator.numeral ℒₒᵣ⋆ n)) <
        !!(Semiterm.Operator.const Semiterm.Operator.Star.star)”)
⊢ ↑n < ⋆

State before:
n : ℕ
this :
  ℕ⋆ ⊧ₘ
    (“!!(Semiterm.Operator.const (Semiterm.Operator.numeral ℒₒᵣ⋆ n)) <
        !!(Semiterm.Operator.const Semiterm.Operator.Star.star)”)
⊢ ↑n < ⋆
Tactic:
simpa [models_iff, Model.numeral_eq_natCast] using this
State after:
no goals