-- Mathlib/Analysis/CStarAlgebra/Matrix.lean
lemma l2_opNorm_mul (A : Matrix m n 𝕜) (B : Matrix n l 𝕜) :
    ‖A * B‖ ≤ ‖A‖ * ‖B‖

Proof state:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
⊢ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) (A * B)‖ ≤
    ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖

Tactic:
have := (toEuclideanLin (n := n) (m := m) (𝕜 := 𝕜) ≪≫ₗ toContinuousLinearMap) A
  |>.opNorm_comp_le <| (toEuclideanLin (n := l) (m := n) (𝕜 := 𝕜) ≪≫ₗ toContinuousLinearMap) B

Result:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
this :
  ‖((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)‖ ≤
    ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖
⊢ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) (A * B)‖ ≤
    ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖

Proof state:
case h.e'_3.h.e'_3.h
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
this :
  ‖((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)‖ ≤
    ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖
x : EuclideanSpace 𝕜 l
⊢ ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) (A * B)) x =
    (((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)) x

Tactic:
exact congr($(Matrix.toLin'_mul A B) x)

Result:
no goals

Proof state:
case h.e'_3.h.e'_3
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
this :
  ‖((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)‖ ≤
    ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖
⊢ (toEuclideanLin ≪≫ₗ toContinuousLinearMap) (A * B) =
    ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)

Tactic:
ext1 x

Result:
case h.e'_3.h.e'_3.h
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
this :
  ‖((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)‖ ≤
    ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖
x : EuclideanSpace 𝕜 l
⊢ ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) (A * B)) x =
    (((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)) x

Proof state:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
⊢ ‖A * B‖ ≤ ‖A‖ * ‖B‖

Tactic:
simp only [l2_opNorm_def]

Result:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
⊢ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) (A * B)‖ ≤
    ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖

Proof state:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
this :
  ‖((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)‖ ≤
    ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖
⊢ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) (A * B)‖ ≤
    ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖

Tactic:
convert this

Result:
case h.e'_3.h.e'_3
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
this :
  ‖((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)‖ ≤
    ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖
⊢ (toEuclideanLin ≪≫ₗ toContinuousLinearMap) (A * B) =
    ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A).comp ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) B)