fix: ignore no_index around OfNat.ofNat in norm_cast (#6438)

This PR ensures `norm_cast` doesn't fail to act in the presence of
`no_index` annotations

While #2867 exists, it is necessary to put `no_index`
around `OfNat.ofNat` in simp lemmas.
This results in extra `Expr.mdata` nodes, which must be removed before
checking for `ofNat` numerals.

Author: eric-wieser

src/Lean/Elab/Tactic/NormCast.lean

@@ -63,7 +63,7 @@ def isNumeral? (e : Expr) : Option (Expr × Nat) :=
   if e.isConstOf ``Nat.zero then
     (mkConst ``Nat, 0)
   else if let Expr.app (Expr.app (Expr.app (Expr.const ``OfNat.ofNat ..) α ..)
-      (Expr.lit (Literal.natVal n) ..) ..) .. := e then
+      (Expr.lit (Literal.natVal n) ..) ..) .. := e.consumeMData then
     some (α, n)
   else
     none