Can norm_cast be made to work on n - 1 + 1?

Stream: Is there code for X?

[Geoffrey Irving]

Is there a way to make norm_cast <$> omega resolve this lemma?

import Mathlib

lemma WithTopENat.sub_add_le {n : ℕ} {n1 : 1 ≤ n} : n - 1 + 1 ≤ (n : WithTop ℕ∞) := by
  norm_cast  -- Doesn't do anything
  omega  -- Doesn't work, since still over WithTop ℕ∞

[Damiano Testa]

It seems that

  rw [← WithTop.coe_one]

is "missing".

[Jovan Gerbscheid]

I think the issue is that norm_cast can't work with the coercion from ℕ to WithTop ℕ∞ very well. The trick @Damiano Testa suggests is to split up the coercion by letting it go via the intermediate type ℕ∞.

[Geoffrey Irving]

I don’t think I fully understood @Damiano Testa’s comment: is it “there’s no way norm_cast can do this so we need to help it”? My initial reading was that adding that kind of lemma would help norm_cast be more automated. (I should clarify that I do have plenty of manual ways to help norm_cast already.)

[Eric Wieser]

set_option trace.Tactic.norm_cast true helps see what is happening

[Jovan Gerbscheid]

Yes, he means that you can add the extra rw tactic to help norm_cast

[Eric Wieser]

This also works:

import Mathlib

@[norm_cast]
theorem WithTop.some_natCast [AddMonoidWithOne α] {n : ℕ} : (n : α) = (n : WithTop α) := rfl

lemma WithTopENat.sub_add_le {n : ℕ} {n1 : 1 ≤ n} : n - 1 + 1 ≤ (n : WithTop ℕ∞) := by
  rw [← WithTop.some_natCast]
  norm_cast
  omega