Theorem: LinearMap.spectral_theorem' (CvxLean/Lib/Math/Analysis/InnerProductSpace/Spectrum.lean)

State before:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : DecidableEq 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
v : E
i : Fin n
xs : OrthonormalBasis (Fin n) 𝕜 E
as : Fin n → ℝ
hxs : ∀ (j : Fin n), Module.End.HasEigenvector T (↑(as j)) (xs j)
⊢ xs.repr (T v) i = ↑(as i) * xs.repr v i
Tactic:
suffices hsuff : ∀ (w : EuclideanSpace 𝕜 (Fin n)),
  T (xs.repr.symm w) = xs.repr.symm (fun i => as i * w i) by
    simpa only [LinearIsometryEquiv.symm_apply_apply,
      LinearIsometryEquiv.apply_symm_apply]
      using congr_arg (fun (v : E) => (xs.repr) v i) (hsuff ((xs.repr) v))
State after:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : DecidableEq 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
v : E
i : Fin n
xs : OrthonormalBasis (Fin n) 𝕜 E
as : Fin n → ℝ
hxs : ∀ (j : Fin n), Module.End.HasEigenvector T (↑(as j)) (xs j)
⊢ ∀ (w : EuclideanSpace 𝕜 (Fin n)), T (xs.repr.symm w) = xs.repr.symm fun i => ↑(as i) * w i

State before:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : DecidableEq 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
v : E
i : Fin n
xs : OrthonormalBasis (Fin n) 𝕜 E
as : Fin n → ℝ
hxs : ∀ (j : Fin n), Module.End.HasEigenvector T (↑(as j)) (xs j)
⊢ ∀ (w : EuclideanSpace 𝕜 (Fin n)), T (xs.repr.symm w) = xs.repr.symm fun i => ↑(as i) * w i
Tactic:
intros w
State after:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : DecidableEq 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
v : E
i : Fin n
xs : OrthonormalBasis (Fin n) 𝕜 E
as : Fin n → ℝ
hxs : ∀ (j : Fin n), Module.End.HasEigenvector T (↑(as j)) (xs j)
w : EuclideanSpace 𝕜 (Fin n)
⊢ T (xs.repr.symm w) = xs.repr.symm fun i => ↑(as i) * w i

State before:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : DecidableEq 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
v : E
i : Fin n
xs : OrthonormalBasis (Fin n) 𝕜 E
as : Fin n → ℝ
hxs : ∀ (j : Fin n), Module.End.HasEigenvector T (↑(as j)) (xs j)
w : EuclideanSpace 𝕜 (Fin n)
⊢ T (xs.repr.symm w) = xs.repr.symm fun i => ↑(as i) * w i
Tactic:
simp_rw [← OrthonormalBasis.sum_repr_symm, map_sum, LinearMap.map_smul,
  fun j => Module.End.mem_eigenspace_iff.mp (hxs j).1, smul_smul, mul_comm]
State after:
no goals

State before:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : DecidableEq 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
v : E
i : Fin n
xs : OrthonormalBasis (Fin n) 𝕜 E
as : Fin n → ℝ
hxs : ∀ (j : Fin n), Module.End.HasEigenvector T (↑(as j)) (xs j)
hsuff : ∀ (w : EuclideanSpace 𝕜 (Fin n)), T (xs.repr.symm w) = xs.repr.symm fun i => ↑(as i) * w i
⊢ xs.repr (T v) i = ↑(as i) * xs.repr v i
Tactic:
simpa only [LinearIsometryEquiv.symm_apply_apply,
  LinearIsometryEquiv.apply_symm_apply]
  using congr_arg (fun (v : E) => (xs.repr) v i) (hsuff ((xs.repr) v))
State after:
no goals