-- Mathlib/Analysis/InnerProductSpace/Spectrum.lean
theorem hasEigenvector_eigenvectorBasis (i : Fin n) :
    HasEigenvector T (hT.eigenvalues hn i) (hT.eigenvectorBasis hn i)

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
n : ℕ
hn : Module.finrank 𝕜 E = n
i : Fin n
v : E := (hT.eigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
key : HasEigenvector T μ v
⊢ HasEigenvector T (↑(RCLike.re μ)) v

Tactic:
have re_μ : ↑(RCLike.re μ) = μ := by
  rw [← RCLike.conj_eq_iff_re]
  exact hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector key)

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
n : ℕ
hn : Module.finrank 𝕜 E = n
i : Fin n
v : E := (hT.eigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
key : HasEigenvector T μ v
re_μ : ↑(RCLike.re μ) = μ
⊢ HasEigenvector T (↑(RCLike.re μ)) v

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
n : ℕ
hn : Module.finrank 𝕜 E = n
i : Fin n
v : E := (hT.eigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
⊢ HasEigenvector T μ v

Tactic:
have H₁ : v ∈ eigenspace T μ := by
  simp_rw [v, eigenvectorBasis]
  exact
    hT.direct_sum_isInternal.subordinateOrthonormalBasis_subordinate hn i
      hT.orthogonalFamily_eigenspaces'

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
n : ℕ
hn : Module.finrank 𝕜 E = n
i : Fin n
v : E := (hT.eigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
H₁ : v ∈ eigenspace T μ
⊢ HasEigenvector T μ v

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
n : ℕ
hn : Module.finrank 𝕜 E = n
i : Fin n
v : E := (hT.eigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
⊢ v ∈ eigenspace T μ

Tactic:
simp_rw [v, eigenvectorBasis]

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
n : ℕ
hn : Module.finrank 𝕜 E = n
i : Fin n
v : E := (hT.eigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
⊢ (DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯) i ∈ eigenspace T μ

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
n : ℕ
hn : Module.finrank 𝕜 E = n
i : Fin n
v : E := (hT.eigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
⊢ (DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯) i ∈ eigenspace T μ

Tactic:
exact
  hT.direct_sum_isInternal.subordinateOrthonormalBasis_subordinate hn i
    hT.orthogonalFamily_eigenspaces'

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
n : ℕ
hn : Module.finrank 𝕜 E = n
i : Fin n
v : E := (hT.eigenvectorBasis hn) i
⊢ HasEigenvector T (↑(hT.eigenvalues hn i)) ((hT.eigenvectorBasis hn) i)

Tactic:
let μ : 𝕜 :=
  (hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
    hT.orthogonalFamily_eigenspaces').val

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
n : ℕ
hn : Module.finrank 𝕜 E = n
i : Fin n
v : E := (hT.eigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
⊢ HasEigenvector T (↑(hT.eigenvalues hn i)) ((hT.eigenvectorBasis hn) i)