chore(Data/Int/WithZero): remove an erw (#38680)

- makes `map_one'` explicit about `WithZero.unzero` at `1`, so the proof is a plain `rw` chain

Extracted from #38415

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/Data/Int/WithZero.lean

@@ -45,9 +45,7 @@ namespace WithZeroMulInt
 def toNNReal {e : ℝ≥0} (he : e ≠ 0) : ℤᵐ⁰ →*₀ ℝ≥0 where
   toFun := fun x ↦ if hx : x = 0 then 0 else e ^ (WithZero.unzero hx).toAdd
   map_zero' := rfl
-  map_one' := by
-    simp only [dif_neg one_ne_zero]
-    erw [toAdd_one, zpow_zero]
+  map_one' := by rw [dif_neg one_ne_zero, unzero_coe (x := 1), toAdd_one, zpow_zero]
   map_mul' x y := by
     by_cases hxy : x * y = 0
     · rcases mul_eq_zero.mp hxy with hx | hy