α : Type u_1
β : Type ?u.382793
γ : Type ?u.382796
ι : Type ?u.382799
inst✝ : SeminormedAddCommGroup α
a : α
⊢ { val := ‖a‖, property := (_ : 0 ≤ ‖a‖) } = ‖a‖₊
α : Type u_1
β : Type ?u.382793
γ : Type ?u.382796
ι : Type ?u.382799
inst✝ : SeminormedAddCommGroup α
a : α
⊢ ‖‖a‖‖₊ = ‖a‖₊
rw [Real.nnnorm_of_nonneg (norm_nonneg a)]
no goals
α : Type u_1
β : Type ?u.382793
γ : Type ?u.382796
ι : Type ?u.382799
inst✝ : SeminormedAddCommGroup α
a : α
⊢ { val := ‖a‖, property := (_ : 0 ≤ ‖a‖) } = ‖a‖₊
rfl