norm_cast gives Int.subNatNat

Stream: mathlib4

[Eric Wieser]

Is this really the behavior we want?

import Mathlib

example (n : ℕ) : (n : ℤ) - 1 = 3 := by
  norm_cast
  /-
  n : ℕ
  ⊢ Int.subNatNat n 1 = 3
  -/
  sorry

[Yury G. Kudryashov]

Which lemma does it use?

[Ruben Van de Velde]

I thought that was fixed

[Ruben Van de Velde]

Ref https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/norm_cast.20leaks.20Int.2EsubSubNat

[Eric Wieser]

Yury G. Kudryashov said:

Which lemma does it use?

docs#Int.cast_subNatNat

[Terence Tao]

As an (inelegant) workaround one can rw [Int.subNatNat_eq_coe] immediately afterwards.

[Yaël Dillies]

I'm pretty sure norm_cast has several kinds of tagging internally and you can specify what kind a specific lemma is. This changes the way norm_cast/push_cast use those lemmas (in particular, whether norm_cast is allowed to use them backwards).

[Yaël Dillies]

I just hit this again. Would be good to fix it

[Ruben Van de Velde]

I thought I filed this, but it was #11573 instead