case a
α : Type ?u.381131
β : Type ?u.381134
γ : Type ?u.381137
ι : Type ?u.381140
x y : ℝ
hx : 0 ≤ x
⊢ ↑(toNNReal x * ‖y‖₊) = ↑‖x * y‖₊
α : Type ?u.381131
β : Type ?u.381134
γ : Type ?u.381137
ι : Type ?u.381140
x y : ℝ
hx : 0 ≤ x
⊢ toNNReal x * ‖y‖₊ = ‖x * y‖₊
ext
no goals
case a
α : Type ?u.381131
β : Type ?u.381134
γ : Type ?u.381137
ι : Type ?u.381140
x y : ℝ
hx : 0 ≤ x
⊢ ↑(toNNReal x * ‖y‖₊) = ↑‖x * y‖₊
simp only [NNReal.coe_mul, nnnorm_mul, coe_nnnorm, Real.toNNReal_of_nonneg, norm_of_nonneg, hx,
  coe_mk]