no goals
𝓕 : Type ?u.1228006
𝕜 : Type ?u.1228009
α : Type ?u.1228012
ι : Type ?u.1228015
κ : Type ?u.1228018
E : Type u_1
F : Type ?u.1228024
G : Type ?u.1228027
inst✝¹ : NormedGroup E
inst✝ : NormedGroup F
a b : E
⊢ ‖a‖₊ = 0 ↔ a = 1
rw [← NNReal.coe_eq_zero, coe_nnnorm', norm_eq_zero'']