omega and casting

Stream: new members

[Sorrachai Yingchareonthawornchai]

Do you know why omega/ring cannot solve this?

theorem le_t_extend {t : ℕ} [inst : NeZero t] : 1 ≤ 2 * (t : ℕ∞) - 1 := by sorry

[Kyle Miller]

ring doesn't prove inequalities, and omega doesn't know about NeZero or the extended naturals.

import Mathlib

theorem le_t_extend {t : ℕ} [inst : NeZero t] : 1 ≤ 2 * (t : ℕ∞) - 1 := by
  have := inst.ne
  norm_cast
  omega

[Vasilii Nesterov]

While norm_cast is the right tactic here, we also have enat_to_nat, which was specifically created to allow using omega with extended naturals. For example:

import Mathlib

theorem le_t_extend {t : ℕ∞} [inst : NeZero t] : 1 ≤ 2 * t - 1 := by
  have := inst.ne
  enat_to_nat
  omega