-- Mathlib/Analysis/InnerProductSpace/Spectrum.lean
theorem diagonalization_apply_self_apply (v : E) (μ : Eigenvalues T) :
    hT.diagonalization (T v) μ = (μ : 𝕜) • hT.diagonalization 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
v : E
μ : Eigenvalues T
this :
  ∀ (w : PiLp 2 fun μ => ↥(eigenspace T (↑T 1 μ))),
    T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => ↑T 1 μ • w μ
⊢ hT.diagonalization (T v) μ = ↑T 1 μ • hT.diagonalization v μ

Tactic:
simpa only [LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.apply_symm_apply] using
  congr_arg (fun w => hT.diagonalization w μ) (this (hT.diagonalization v))

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
v : E
μ : Eigenvalues T
⊢ ∀ (w : PiLp 2 fun μ => ↥(eigenspace T (↑T 1 μ))),
    T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => ↑T 1 μ • w μ

Tactic:
intro w

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
v : E
μ : Eigenvalues T
w : PiLp 2 fun μ => ↥(eigenspace T (↑T 1 μ))
⊢ T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => ↑T 1 μ • w μ

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
v : E
μ : Eigenvalues T
w : PiLp 2 fun μ => ↥(eigenspace T (↑T 1 μ))
⊢ T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => ↑T 1 μ • w μ

Tactic:
have hwT : ∀ μ, T (w μ) = (μ : 𝕜) • w μ := fun μ => mem_eigenspace_iff.1 (w μ).2

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
v : E
μ : Eigenvalues T
w : PiLp 2 fun μ => ↥(eigenspace T (↑T 1 μ))
hwT : ∀ (μ : Eigenvalues T), T ↑(w μ) = ↑T 1 μ • ↑(w μ)
⊢ T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => ↑T 1 μ • w μ

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
v : E
μ : Eigenvalues T
w : PiLp 2 fun μ => ↥(eigenspace T (↑T 1 μ))
hwT : ∀ (μ : Eigenvalues T), T ↑(w μ) = ↑T 1 μ • ↑(w μ)
⊢ T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => ↑T 1 μ • w μ

Tactic:
simp only [hwT, diagonalization_symm_apply, map_sum, Submodule.coe_smul_of_tower]

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
v : E
μ : Eigenvalues T
⊢ hT.diagonalization (T v) μ = ↑T 1 μ • hT.diagonalization v μ

Tactic:
suffices
  ∀ w : PiLp 2 fun μ : Eigenvalues T => eigenspace T μ,
    T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => (μ : 𝕜) • w μ by
  simpa only [LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.apply_symm_apply] using
    congr_arg (fun w => hT.diagonalization w μ) (this (hT.diagonalization v))

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
v : E
μ : Eigenvalues T
⊢ ∀ (w : PiLp 2 fun μ => ↥(eigenspace T (↑T 1 μ))),
    T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => ↑T 1 μ • w μ