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