-- Mathlib/Analysis/Matrix.lean
theorem linfty_opNNNorm_mul (A : Matrix l m α) (B : Matrix m n α) : ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.univ.sup fun i => ∑ j : m, ‖A i j‖₊ * Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊) ≤
    (Finset.univ.sup fun i => ∑ j : m, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊

Tactic:
simp_rw [← Finset.sum_mul, ← NNReal.finset_sup_mul]

Result:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ ((Finset.univ.sup fun a => ∑ i : m, ‖A a i‖₊) * Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊) ≤
    (Finset.univ.sup fun i => ∑ j : m, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ ((Finset.univ.sup fun a => ∑ i : m, ‖A a i‖₊) * Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊) ≤
    (Finset.univ.sup fun i => ∑ j : m, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊

Tactic:
rfl

Result:
no goals

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : i ∈ Finset.univ
⊢ ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊ ≤ ∑ j : m, ‖A i j‖₊ * Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊

Tactic:
gcongr with j hj

Result:
case h.bc
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : i ∈ Finset.univ
j : m
hj : j ∈ Finset.univ
⊢ ∑ k : n, ‖B j k‖₊ ≤ Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.univ.sup fun i => ∑ x : n, ‖∑ j : m, A i j * B j x‖₊) ≤
    (Finset.univ.sup fun i => ∑ j : m, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊

Tactic:
calc
  (Finset.univ.sup fun i => ∑ k, ‖∑ j, A i j * B j k‖₊) ≤
      Finset.univ.sup fun i => ∑ k, ∑ j, ‖A i j‖₊ * ‖B j k‖₊ :=
    Finset.sup_mono_fun fun i _hi =>
      Finset.sum_le_sum fun k _hk => nnnorm_sum_le_of_le _ fun j _hj => nnnorm_mul_le _ _
  _ = Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊ := by
    simp_rw [@Finset.sum_comm m, Finset.mul_sum]
  _ ≤ Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ := by
    refine Finset.sup_mono_fun fun i _hi => ?_
    gcongr with j hj
    exact Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj
  _ ≤ (Finset.univ.sup fun i => ∑ j, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ := by
    simp_rw [← Finset.sum_mul, ← NNReal.finset_sup_mul]
    rfl

Result:
no goals

Proof state:
case h.bc
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : i ∈ Finset.univ
j : m
hj : j ∈ Finset.univ
⊢ ∑ k : n, ‖B j k‖₊ ≤ Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊

Tactic:
exact Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj

Result:
no goals

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.univ.sup fun i => ∑ k : n, ∑ j : m, ‖A i j‖₊ * ‖B j k‖₊) =
    Finset.univ.sup fun i => ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊

Tactic:
simp_rw [@Finset.sum_comm m, Finset.mul_sum]

Result:
no goals

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

Tactic:
simp_rw [linfty_opNNNorm_def, Matrix.mul_apply]

Result:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.univ.sup fun i => ∑ x : n, ‖∑ j : m, A i j * B j x‖₊) ≤
    (Finset.univ.sup fun i => ∑ j : m, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.univ.sup fun i => ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊) ≤
    Finset.univ.sup fun i => ∑ j : m, ‖A i j‖₊ * Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊

Tactic:
refine Finset.sup_mono_fun fun i _hi => ?_

Result:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : i ∈ Finset.univ
⊢ ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊ ≤ ∑ j : m, ‖A i j‖₊ * Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊