norm_cast weakness

Stream: mathlib4

[Michael Stoll]

import Mathlib.Topology.Instances.ENNReal

open NNReal ENNReal Filter Topology

lemma foo (r : ℝ≥0) (h : Tendsto (fun n ↦ (r ^ n : ℝ≥0∞)) atTop (𝓝 0)) :
    Tendsto (fun n ↦ r ^ n) atTop (𝓝 0) := by
  -- exact_mod_cast h  -- does not work
  rw [← ENNReal.coe_zero] at h
  exact_mod_cast h -- now works

Can it be arranged that norm_cast automatically un-coerces 0 (and similarly, 1) when necessary to be able to apply something like tendsto_coe?