-- Mathlib/Analysis/Matrix.lean
theorem frobenius_nnnorm_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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
⊢ ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

Tactic:
simp_rw [frobenius_nnnorm_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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
⊢ (∑ x : l, ∑ x_1 : n, ‖∑ j : m, A x j * B j x_1‖₊ ^ 2) ^ (1 / 2) ≤
    (∑ i : l, ∑ j : m, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ i : m, ∑ j : n, ‖B i j‖₊ ^ 2) ^ (1 / 2)

Proof state:
case h₁.h.h
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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
i : l
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
this :
  ‖inner ((WithLp.equiv 2 (m → α)).symm fun j => star (A i j)) ((WithLp.equiv 2 (m → α)).symm fun k => B k j)‖₊ ≤
    ‖(WithLp.equiv 2 (m → α)).symm fun j => star (A i j)‖₊ * ‖(WithLp.equiv 2 (m → α)).symm fun k => B k j‖₊
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ≤ (∑ j : m, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ x : m, ‖B x j‖₊ ^ 2) ^ (1 / 2)

Tactic:
simpa only [WithLp.equiv_symm_pi_apply, PiLp.inner_apply, RCLike.inner_apply, starRingEnd_apply,
  Pi.nnnorm_def, PiLp.nnnorm_eq_of_L2, star_star, nnnorm_star, NNReal.sqrt_eq_rpow,
  NNReal.rpow_two] using this

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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
⊢ (∑ x : l, ∑ x_1 : n, ‖∑ j : m, A x j * B j x_1‖₊ ^ 2) ^ (1 / 2) ≤
    (∑ i : l, ∑ j : m, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ i : m, ∑ j : n, ‖B i j‖₊ ^ 2) ^ (1 / 2)

Tactic:
rw [← NNReal.mul_rpow, @Finset.sum_comm _ _ m, Finset.sum_mul_sum]

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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
⊢ (∑ x : l, ∑ x_1 : n, ‖∑ j : m, A x j * B j x_1‖₊ ^ 2) ^ (1 / 2) ≤
    (∑ i : l, ∑ j : n, (∑ j : m, ‖A i j‖₊ ^ 2) * ∑ x : m, ‖B x j‖₊ ^ 2) ^ (1 / 2)

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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
⊢ (∑ x : l, ∑ x_1 : n, ‖∑ j : m, A x j * B j x_1‖₊ ^ 2) ^ (1 / 2) ≤
    (∑ i : l, ∑ j : n, (∑ j : m, ‖A i j‖₊ ^ 2) * ∑ x : m, ‖B x j‖₊ ^ 2) ^ (1 / 2)

Tactic:
gcongr with i _ j

Result:
case h₁.h.h
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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
i : l
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ^ 2 ≤ (∑ j : m, ‖A i j‖₊ ^ 2) * ∑ x : m, ‖B x j‖₊ ^ 2

Proof state:
case h₁.h.h
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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
i : l
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ≤ (∑ j : m, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ x : m, ‖B x j‖₊ ^ 2) ^ (1 / 2)

Tactic:
have :=
  @nnnorm_inner_le_nnnorm α _ _ _ _ ((WithLp.equiv 2 <| _ → α).symm fun j => star (A i j))
    ((WithLp.equiv 2 <| _ → α).symm fun k => B k j)

Result:
case h₁.h.h
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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
i : l
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
this :
  ‖inner ((WithLp.equiv 2 (m → α)).symm fun j => star (A i j)) ((WithLp.equiv 2 (m → α)).symm fun k => B k j)‖₊ ≤
    ‖(WithLp.equiv 2 (m → α)).symm fun j => star (A i j)‖₊ * ‖(WithLp.equiv 2 (m → α)).symm fun k => B k j‖₊
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ≤ (∑ j : m, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ x : m, ‖B x j‖₊ ^ 2) ^ (1 / 2)

Proof state:
case h₁.h.h
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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
i : l
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ^ 2 ≤ (∑ j : m, ‖A i j‖₊ ^ 2) * ∑ x : m, ‖B x j‖₊ ^ 2

Tactic:
rw [← NNReal.rpow_le_rpow_iff one_half_pos, ← NNReal.rpow_mul,
  mul_div_cancel₀ (1 : ℝ) two_ne_zero, NNReal.rpow_one, NNReal.mul_rpow]

Result:
case h₁.h.h
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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
i : l
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ≤ (∑ j : m, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ x : m, ‖B x j‖₊ ^ 2) ^ (1 / 2)