no goals
𝓕 : Type ?u.1109014
𝕜 : Type ?u.1109017
α : Type ?u.1109020
ι : Type ?u.1109023
κ : Type ?u.1109026
E : Type ?u.1109029
F : Type ?u.1109032
G : Type ?u.1109035
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r✝ r₁ r₂ r : ℝ
⊢ ↑‖r‖₊ = ENNReal.ofReal (abs r)
rw [← Real.nnnorm_abs r, Real.ennnorm_eq_ofReal (abs_nonneg _)]