Theorem: Matrix.IsHermitian.spectral_theorem'' (CvxLean/Lib/Math/Subadditivity.lean)

State before:
n : Type u_1
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : LinearOrder n
inst✝² : LocallyFiniteOrderBot n
𝕜 : Type u_2
inst✝¹ : DecidableEq 𝕜
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ hA.eigenvectorMatrix * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * hA.eigenvectorMatrix.conjTranspose = A
Tactic:
rw [conjTranspose_eigenvectorMatrix, Matrix.mul_assoc, ← spectral_theorem,
  ← Matrix.mul_assoc, eigenvectorMatrix_mul_inv, Matrix.one_mul]
State after:
no goals