Lean rw [← h] with h : a = 1 can fail on goals containing (2 : ℝ)

Lean v4.35 + Mathlib. In ℝ, ℂ, ENNReal and ZMod n, a numeral n ≥ 2 elaborates as @OfNat.ofNat ℝ n (instOfNatAtLeastTwo ..) whose hidden instance proof contains the ℕ literals n-1 and n-2 (set_option pp.explicit true plus pp.proofs true shows (100 : ℝ) carrying 99 and 98). So with a : ℕ and h : a = k, rw [← h] fails with 'motive is not type correct' if the goal contains the numeral k+1 or k+2 in one of those types, even with no visible k: h : a = 1 breaks on 2 * x = 5 and on (3 : ℝ), h : a = 0 on (2 : ℝ), h : a = 98 on (100 : ℝ), while h : a = 97 just reports 'did not find'. Unaffected in my tests: ℚ and ℤ (their own OfNat instances). Fixes that worked: rewrite forwards in the hypothesis (rw [h] at hx), subst h, or simp only [← h]; nth_rw 1 [← h] picks the hidden occurrence and fails the same way. Typical trigger: rw [← hg] with hg : Nat.gcd m n = 1 to turn (2 : ZMod p) ^ 1 into 2 ^ gcd m n; instead have := pow_gcd_eq_one.2 ⟨h1, h2⟩; rw [hg, pow_one] at this.