𝓕 : Type ?u.321774
𝕜 : Type ?u.321777
α : Type ?u.321780
ι : Type ?u.321783
κ : Type ?u.321786
E : Type u_1
F : Type ?u.321792
G : Type ?u.321795
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ ‖1‖₊ = 0
𝓕 : Type ?u.321774
𝕜 : Type ?u.321777
α : Type ?u.321780
ι : Type ?u.321783
κ : Type ?u.321786
E : Type u_1
F : Type ?u.321792
G : Type ?u.321795
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
a : E
⊢ a = 1 → ‖a‖₊ = 0
rintro rfl
no goals
𝓕 : Type ?u.321774
𝕜 : Type ?u.321777
α : Type ?u.321780
ι : Type ?u.321783
κ : Type ?u.321786
E : Type u_1
F : Type ?u.321792
G : Type ?u.321795
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ ‖1‖₊ = 0
exact nnnorm_one'