no goals
𝓕 : Type ?u.1108722
𝕜 : Type ?u.1108725
α : Type ?u.1108728
ι : Type ?u.1108731
κ : Type ?u.1108734
E : Type ?u.1108737
F : Type ?u.1108740
G : Type ?u.1108743
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
hr : 0 ≤ r
⊢ ↑‖r‖₊ = ENNReal.ofReal r
rw [← ofReal_norm_eq_coe_nnnorm, norm_of_nonneg hr]