no goals
𝓕 : Type ?u.1227402
𝕜 : Type ?u.1227405
α : Type ?u.1227408
ι : Type ?u.1227411
κ : Type ?u.1227414
E : Type u_1
F : Type ?u.1227420
G : Type ?u.1227423
inst✝¹ : NormedGroup E
inst✝ : NormedGroup F
a b : E
h : ‖a / b‖ ≤ 0
⊢ a = b
rwa [← div_eq_one, ← norm_le_zero_iff'']