no goals
𝓕 : Type ?u.1107777
𝕜 : Type ?u.1107780
α : Type ?u.1107783
ι : Type ?u.1107786
κ : Type ?u.1107789
E : Type ?u.1107792
F : Type ?u.1107795
G : Type ?u.1107798
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ ↑‖2‖₊ = ↑2
simp