-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
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‖
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖
have 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‖
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 _