doc: describe why map_ofNat can't be simp (yet) (#19410)

See the benchmark in #19388, which while not disastrous is not ideal either.

Unless the situation changes with leanprover/lean4#2867, the DiscrTree key would apply to all funlike operations applied to any argument, not just applied to numerals.

Author: eric-wieser

Mathlib/Data/Nat/Cast/Basic.lean

@@ -159,6 +159,11 @@ theorem eq_natCast [FunLike F ℕ R] [RingHomClass F ℕ R] (f : F) : ∀ n, f n
 theorem map_natCast [FunLike F R S] [RingHomClass F R S] (f : F) : ∀ n : ℕ, f (n : R) = n :=
   map_natCast' f <| map_one f
 
+/-- This lemma is not marked `@[simp]` lemma because its `#discr_tree_key` (for the LHS) would just
+be `DFunLike.coe _ _`, due to the `no_index` that https://github.com/leanprover/lean4/issues/2867
+forces us to include, and therefore it would negatively impact performance.
+
+If that issue is resolved, this can be marked `@[simp]`. -/
 theorem map_ofNat [FunLike F R S] [RingHomClass F R S] (f : F) (n : ℕ) [Nat.AtLeastTwo n] :
     (f (no_index (OfNat.ofNat n)) : S) = OfNat.ofNat n :=
   map_natCast f n