norm_cast leaks Int.subSubNat

Stream: mathlib4

[Yaël Dillies]

Why does norm_cast put a Int.subSubNat in the goal?

import Mathlib.Tactic.NormNum

variable (a b : ℕ)

example : (1 : ℕ) + (↑(max a b) - ↑(min a b)) = Int.ofNat (Int.natAbs (↑b - ↑a) + 1) := by
  norm_cast
  sorry

Interestingly, as I was reducing imports, norm_cast went from putting int.subSubNat in the goal to being a no-op back and forth several times.

[Yaël Dillies]

From doing show_term, the culprit seems to be Mathlib.Data.Int.Cast.Basic._auxLemma.5, which I cannot even #print.

[Kyle Miller]

simp-like tactics can transform simp lemmas to put them into a better form, and it gives them _auxLemma.nnn names. Lean doesn't let you type in names with numbers, and I'm not aware of any way to write them yourself. (They're not names with numeral strings, but a completely different kind of part of a name.)

Here's a special hacked-together #print that you can use to get their definitions:

open Lean in
elab "#printNum " n:ident i:num : command => do
  let name := Name.num n.getId i.getNat
  let some decl := (← getEnv).find? name | throwError "no such declaration {name}"
  logInfo m!"{name} : {decl.type} :=\n{decl.value?.getD (.bvar 0)}"

#printNum Mathlib.Data.Int.Cast.Basic._auxLemma 5
/-
Mathlib.Data.Int.Cast.Basic._auxLemma.5 : ∀ {R : Type u} [inst : AddGroupWithOne R] (m n : ℕ),
  ↑m - ↑n = ↑(Int.subNatNat m n) :=
fun {R} [AddGroupWithOne R] m n ↦ Eq.symm (Int.cast_subNatNat m n)
-/

[Kyle Miller]

So this auxLemma is wrapping Int.cast_subNatNat