-- Mathlib/LinearAlgebra/Matrix/Spectrum.lean
theorem star_mul_self_mul_eq_diagonal :
    (star (eigenvectorUnitary hA : Matrix n n 𝕜)) * A * (eigenvectorUnitary hA : Matrix n n 𝕜)
      = diagonal (RCLike.ofReal ∘ hA.eigenvalues)

Proof state:
case a.h
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ ∀ (i_1 : n), (↑(hA.eigenvalues i) • EuclideanSpace.single i 1) i_1 = EuclideanSpace.single i (↑(hA.eigenvalues i)) i_1

Tactic:
intro j

Result:
case a.h
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i j : n
⊢ (↑(hA.eigenvalues i) • EuclideanSpace.single i 1) j = EuclideanSpace.single i (↑(hA.eigenvalues i)) j

Proof state:
case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ ∀ (i : n),
    (toEuclideanLin (star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary))
        ((EuclideanSpace.basisFun n 𝕜).toBasis i) =
      (toEuclideanLin (diagonal (RCLike.ofReal ∘ hA.eigenvalues))) ((EuclideanSpace.basisFun n 𝕜).toBasis i)

Tactic:
intro i

Result:
case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ (toEuclideanLin (star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary))
      ((EuclideanSpace.basisFun n 𝕜).toBasis i) =
    (toEuclideanLin (diagonal (RCLike.ofReal ∘ hA.eigenvalues))) ((EuclideanSpace.basisFun n 𝕜).toBasis i)

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary = diagonal (RCLike.ofReal ∘ hA.eigenvalues)

Tactic:
apply Matrix.toEuclideanLin.injective

Result:
case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ toEuclideanLin (star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary) =
    toEuclideanLin (diagonal (RCLike.ofReal ∘ hA.eigenvalues))

Proof state:
case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ ↑(hA.eigenvalues i) • EuclideanSpace.single i 1 = EuclideanSpace.single i ↑(hA.eigenvalues i)

Tactic:
apply PiLp.ext

Result:
case a.h
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ ∀ (i_1 : n), (↑(hA.eigenvalues i) • EuclideanSpace.single i 1) i_1 = EuclideanSpace.single i (↑(hA.eigenvalues i)) i_1

Proof state:
case a.h
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i j : n
⊢ (↑(hA.eigenvalues i) • EuclideanSpace.single i 1) j = EuclideanSpace.single i (↑(hA.eigenvalues i)) j

Tactic:
simp only [PiLp.smul_apply, EuclideanSpace.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero]

Result:
no goals

Proof state:
case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ (toEuclideanLin (star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary))
      ((EuclideanSpace.basisFun n 𝕜).toBasis i) =
    (toEuclideanLin (diagonal (RCLike.ofReal ∘ hA.eigenvalues))) ((EuclideanSpace.basisFun n 𝕜).toBasis i)

Tactic:
simp only [toEuclideanLin_apply, OrthonormalBasis.coe_toBasis, EuclideanSpace.basisFun_apply,
  WithLp.equiv_single, ← mulVec_mulVec, eigenvectorUnitary_mulVec, ← mulVec_mulVec,
  mulVec_eigenvectorBasis, Matrix.diagonal_mulVec_single, mulVec_smul,
  star_eigenvectorUnitary_mulVec, RCLike.real_smul_eq_coe_smul (K := 𝕜), WithLp.equiv_symm_smul,
  WithLp.equiv_symm_single, Function.comp_apply, mul_one, WithLp.equiv_symm_single]

Result:
case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ ↑(hA.eigenvalues i) • EuclideanSpace.single i 1 = EuclideanSpace.single i ↑(hA.eigenvalues i)

Proof state:
case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ toEuclideanLin (star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary) =
    toEuclideanLin (diagonal (RCLike.ofReal ∘ hA.eigenvalues))

Tactic:
apply Basis.ext (EuclideanSpace.basisFun n 𝕜).toBasis

Result:
case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ ∀ (i : n),
    (toEuclideanLin (star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary))
        ((EuclideanSpace.basisFun n 𝕜).toBasis i) =
      (toEuclideanLin (diagonal (RCLike.ofReal ∘ hA.eigenvalues))) ((EuclideanSpace.basisFun n 𝕜).toBasis i)