no goals
𝓕 : Type ?u.501471
𝕜 : Type ?u.501474
α : Type ?u.501477
ι : Type ?u.501480
κ : Type ?u.501483
E : Type u_1
F : Type ?u.501489
G : Type ?u.501492
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : SeminormedGroup G
s : Set E
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : T0Space E
a : E
⊢ 0 < ‖a‖ ↔ a ≠ 1
rw [← not_le, norm_le_zero_iff''']