simp_rw [← Finset.univ_product_univ, Finset.sup_product_left, ← Pi.nnnorm_def, coe_nnnorm]
ι : Type ?u.137142
R : Type ?u.137145
l : Type ?u.137148
m : Type u_1
n : Type u_2
p : Type ?u.137157
q : Type ?u.137160
r : Type ?u.137163
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ ‖A‖ = ↑(Finset.univ.sup fun ij => ‖A ij.1 ij.2‖₊)
no goals