-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m n 𝕜
rw :
  norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (Aᴴ * A) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖
rw₁ :
  norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      (((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜)) :
                Matrix n n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≪≫ₗ
              toContinuousLinearMap :
            (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (Aᴴ * A) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖
rw₂ :
  norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      (((toContinuousLinearMap :
              (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
            (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜)) :
                Matrix n n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) :
              (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n)
            (Aᴴ * A)) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖
rw₃ :
  norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      (((toContinuousLinearMap :
              (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
            (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜))
                    (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜)) :
                  Matrix n m 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n) :
                (a : Matrix n m 𝕜) → EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n)
              Aᴴ ∘ₗ
            (toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜)) :
                (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m)
              A) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖
rw₄ rw₅ rw₆ :
  norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      (((toContinuousLinearMap :
              (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
            (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          ((adjoint : (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) → EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n)
              ((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                    (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜)) :
                  (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m)
                A) ∘ₗ
            (toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜)) :
                (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m)
              A) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖

Tactic:
classical
  rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]
  exact ContinuousLinearMap.norm_adjoint_comp_self _

Premises used: Matrix.toLin_mul, LinearEquiv.trans_apply, EuclideanSpace.basisFun, Matrix.toLin_conjTranspose, Matrix.toEuclideanLin_eq_toLin_orthonormal, ContinuousLinearMap.norm_adjoint_comp_self, Matrix.l2_opNorm_def, OrthonormalBasis.toBasis