no goals
𝓕 : Type ?u.1108272
𝕜 : Type ?u.1108275
α : Type ?u.1108278
ι : Type ?u.1108281
κ : Type ?u.1108284
E : Type ?u.1108287
F : Type ?u.1108290
G : Type ?u.1108293
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r✝ r₁ r₂ r : ℝ
⊢ ‖abs r‖₊ = ‖r‖₊
simp [nnnorm]