awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn : (a : Fin n) → E) i
μ : 𝕜 := (↑T : Eigenvalues T → 𝕜) (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
⊢ HasEigenvector T μ v

Tactic:
have key : HasEigenvector T μ v := by
    have H₁ : v ∈ eigenspace T μ := by
      simp_rw [v, unsortedEigenvectorBasis]
      exact
        hT.direct_sum_isInternal.subordinateOrthonormalBasis_subordinate hn i
          hT.orthogonalFamily_eigenspaces'
    have H₂ : v ≠ 0 := by simpa using (hT.unsortedEigenvectorBasis hn).toBasis.ne_zero i
    exact ⟨H₁, H₂⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn : (a : Fin n) → E) i
μ : 𝕜 := (↑T : Eigenvalues T → 𝕜) (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
key : HasEigenvector T μ v
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ) μ) : 𝕜) = μ

Tactic:
rw [← RCLike.conj_eq_iff_re]

Premises used: RCLike.conj_eq_iff_re
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn : (a : Fin n) → E) i
μ : 𝕜 := (↑T : Eigenvalues T → 𝕜) (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
key : HasEigenvector T μ v
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ

Tactic:
hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector key)

Premises used: LinearMap.IsSymmetric.conj_eigenvalue_eq_self, Module.End.hasEigenvalue_of_hasEigenvector
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn : (a : Fin n) → E) i
μ : 𝕜 := (↑T : Eigenvalues T → 𝕜) (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
key : HasEigenvector T μ v
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ

Tactic:
exact hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector key)

Premises used: LinearMap.IsSymmetric.conj_eigenvalue_eq_self, Module.End.hasEigenvalue_of_hasEigenvector
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn : (a : Fin n) → E) i
μ : 𝕜 := (↑T : Eigenvalues T → 𝕜) (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
key : HasEigenvector T μ v
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ) μ) : 𝕜) = μ

Tactic:
have re_μ : ↑(RCLike.re μ) = μ := by
    rw [← RCLike.conj_eq_iff_re]
    exact hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector key)
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn : (a : Fin n) → E) i
μ : 𝕜 := (↑T : Eigenvalues T → 𝕜) (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
key : HasEigenvector T μ v
re_μ : (↑((RCLike.re : (a : 𝕜) → ℝ) μ) : 𝕜) = μ
⊢ HasEigenvector T (↑((RCLike.re : (a : 𝕜) → ℝ) μ) : 𝕜) v

Tactic:
simpa [re_μ] using key
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
μ : 𝕜
hμ : HasEigenvalue T μ
obtain : ∀ (i : Fin n) (hi : (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ), ∃ (i : Fin n), (↑(hT.eigenvalues hn i) : 𝕜) = μ
⊢ ∃ (i : Fin n), (↑(hT.eigenvalues hn i) : 𝕜) = μ

Tactic:
obtain ⟨i, hi⟩ := hT.exists_unsortedEigenvalues_eq hn hμ

Premises used: _private.0.LinearMap.IsSymmetric.exists_unsortedEigenvalues_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
μ : 𝕜
hμ : HasEigenvalue T μ
i : Fin n
hi : (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ
h :
  (↑(hT.eigenvalues hn
          ((Fin.revPerm : (a : Fin n) → Fin n)
            ((Equiv.symm (Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n) i))) :
      𝕜) =
    μ
⊢ ∃ (i : Fin n), (↑(hT.eigenvalues hn i) : 𝕜) = μ

Tactic:
use ((Tuple.sort (hT.unsortedEigenvalues hn)).symm i).revPerm

Premises used: Equiv.symm, _private.0.LinearMap.IsSymmetric.unsortedEigenvalues, DFunLike.coe, Fin.revPerm, Tuple.sort
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
μ : 𝕜
hμ : HasEigenvalue T μ
i : Fin n
hi : (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ
⊢ (↑(hT.eigenvalues hn
          ((Fin.revPerm : (a : Fin n) → Fin n)
            ((Equiv.symm (Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n) i))) :
      𝕜) =
    μ

Tactic:
simp [eigenvalues_def, hi]

Premises used: LinearMap.IsSymmetric.eigenvalues_def
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
μ : 𝕜
rw :
  Finset.card (α := Fin n)
      {i : Fin n |
        (↑((hT.unsortedEigenvalues hn ∘
                  Function.comp (β := Fin n) (⇑(Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n)
                    (⇑Fin.revPerm : (a : Fin n) → Fin n))
                i) :
            𝕜) =
          μ} =
    Finset.card (α := Fin n) {i : Fin n | (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ}
⊢ Finset.card (α := Fin n) {i : Fin n | (↑(hT.eigenvalues hn i) : 𝕜) = μ} = finrank.{u_1, u_2} 𝕜 ↥(eigenspace T μ)

Tactic:
rw [← hT.card_filter_unsortedEigenvalues_eq hn, eigenvalues_def]

Premises used: _private.0.LinearMap.IsSymmetric.card_filter_unsortedEigenvalues_eq, LinearMap.IsSymmetric.eigenvalues_def
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
μ : 𝕜
apply :
  ∀ (i : Fin n),
    Membership.mem (γ := Finset (Fin n))
        {i : Fin n |
          (↑((hT.unsortedEigenvalues hn ∘
                    Function.comp (β := Fin n) (⇑(Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n)
                      (⇑Fin.revPerm : (a : Fin n) → Fin n))
                  i) :
              𝕜) =
            μ}
        i ↔
      Membership.mem (α := Fin n) (γ := Finset (Fin n)) {i : Fin n | (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ}
        ((Equiv.trans Fin.revPerm (Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n) i : Fin n)
⊢ Finset.card (α := Fin n)
      {i : Fin n |
        (↑((hT.unsortedEigenvalues hn ∘
                  Function.comp (β := Fin n) (⇑(Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n)
                    (⇑Fin.revPerm : (a : Fin n) → Fin n))
                i) :
            𝕜) =
          μ} =
    Finset.card (α := Fin n) {i : Fin n | (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ}

Tactic:
apply Finset.card_equiv (Fin.revPerm.trans (Tuple.sort (hT.unsortedEigenvalues hn)))

Premises used: Finset.card_equiv, Equiv.trans, _private.0.LinearMap.IsSymmetric.unsortedEigenvalues, Fin.revPerm, Tuple.sort
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
μ : 𝕜
⊢ ∀ (i : Fin n),
    Membership.mem (γ := Finset (Fin n))
        {i : Fin n |
          (↑((hT.unsortedEigenvalues hn ∘
                    Function.comp (β := Fin n) (⇑(Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n)
                      (⇑Fin.revPerm : (a : Fin n) → Fin n))
                  i) :
              𝕜) =
            μ}
        i ↔
      Membership.mem (α := Fin n) (γ := Finset (Fin n)) {i : Fin n | (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ}
        ((Equiv.trans Fin.revPerm (Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n) i : Fin n)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
i : Fin n
rw :
  HasEigenvector T
    (↑((hT.unsortedEigenvalues hn ∘
            Function.comp (β := Fin n) (⇑(Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n)
              (⇑Fin.revPerm : (a : Fin n) → Fin n))
          i) :
      𝕜)
    ((DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯ : (a : Fin n) → E)
      (((Equiv.symm (Tuple.sort (hT.unsortedEigenvalues hn) * Fin.revPerm)).symm : (a : Fin n) → Fin n) i : Fin n))
⊢ HasEigenvector T (↑(hT.eigenvalues hn i) : 𝕜) ((hT.eigenvectorBasis hn : (a : Fin n) → E) i)

Tactic:
rw [eigenvalues_def, eigenvectorBasis_def, OrthonormalBasis.reindex_apply]

Premises used: OrthonormalBasis.reindex_apply, LinearMap.IsSymmetric.eigenvalues_def, LinearMap.IsSymmetric.eigenvectorBasis_def
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
i : Fin n
⊢ HasEigenvector T
    (↑((hT.unsortedEigenvalues hn ∘
            Function.comp (β := Fin n) (⇑(Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n)
              (⇑Fin.revPerm : (a : Fin n) → Fin n))
          i) :
      𝕜)
    ((DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯ : (a : Fin n) → E)
      (((Equiv.symm (Tuple.sort (hT.unsortedEigenvalues hn) * Fin.revPerm)).symm : (a : Fin n) → Fin n) i : Fin n))

Tactic:
apply hasEigenvector_eigenvectorBasis_helper

Premises used: _private.0.LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis_helper
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
rw :
  Antitone (α := Fin n)
    (Function.comp (β := Fin n)
      (hT.unsortedEigenvalues hn ∘ (⇑(Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n))
      (⇑Fin.revPerm : (a : Fin n) → Fin n))
⊢ Antitone (hT.eigenvalues hn)

Tactic:
rw [eigenvalues_def, ← Function.comp_assoc]

Premises used: LinearMap.IsSymmetric.eigenvalues_def, Function.comp_assoc
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
⊢ Antitone (α := Fin n)
    (Function.comp (β := Fin n)
      (hT.unsortedEigenvalues hn ∘ (⇑(Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n))
      (⇑Fin.revPerm : (a : Fin n) → Fin n))

Tactic:
Monotone.comp_antitone ?_ ?_

Premises used: Monotone.comp_antitone
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
refine_1 :
  Monotone (α := Fin n) (hT.unsortedEigenvalues hn ∘ (⇑(Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n))
refine_2 : Antitone (α := Fin n) (β := Fin n) (⇑Fin.revPerm : (a : Fin n) → Fin n)
⊢ Antitone (α := Fin n)
    (Function.comp (β := Fin n)
      (hT.unsortedEigenvalues hn ∘ (⇑(Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n))
      (⇑Fin.revPerm : (a : Fin n) → Fin n))

Tactic:
refine Monotone.comp_antitone ?_ ?_

Premises used: Monotone.comp_antitone
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
⊢ Monotone (α := Fin n) (hT.unsortedEigenvalues hn ∘ (⇑(Tuple.sort (hT.unsortedEigenvalues hn)) : (a : Fin n) → Fin n))

Tactic:
apply Tuple.monotone_sort

Premises used: Tuple.monotone_sort
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
a : Fin n
refine_2 :
  ∀ ⦃b : Fin n⦄,
    a ≤ b →
      LE.le (α := Fin n) ((Fin.revPerm : (a : Fin n) → Fin n) b : Fin n) ((Fin.revPerm : (a : Fin n) → Fin n) a : Fin n)
⊢ ∀ ⦃b : Fin n⦄,
    a ≤ b →
      LE.le (α := Fin n) ((Fin.revPerm : (a : Fin n) → Fin n) b : Fin n) ((Fin.revPerm : (a : Fin n) → Fin n) a : Fin n)

Tactic:
_
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
a b : Fin n
h : a ≤ b
⊢ LE.le (α := Fin n) ((Fin.revPerm : (a : Fin n) → Fin n) b : Fin n) ((Fin.revPerm : (a : Fin n) → Fin n) a : Fin n)

Tactic:
Fin.rev_le_rev.mpr h

Premises used: Iff.mpr, Fin.rev_le_rev
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
a b : Fin n
h : a ≤ b
⊢ LE.le (α := Fin n) ((Fin.revPerm : (a : Fin n) → Fin n) b : Fin n) ((Fin.revPerm : (a : Fin n) → Fin n) a : Fin n)

Tactic:
exact Fin.rev_le_rev.mpr h

Premises used: Iff.mpr, Fin.rev_le_rev
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
i : Fin n
⊢ HasEigenvalue T (↑(hT.eigenvalues hn i) : 𝕜)

Tactic:
Module.End.hasEigenvalue_of_hasEigenvector (hT.hasEigenvector_eigenvectorBasis hn i)

Premises used: Module.End.hasEigenvalue_of_hasEigenvector, LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
i : Fin n
⊢ (T : (a : E) → E) ((hT.eigenvectorBasis hn : (a : Fin n) → E) i : E) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑(hT.eigenvalues hn i) : 𝕜)
      ((hT.eigenvectorBasis hn : (a : Fin n) → E) i : E)

Tactic:
mem_eigenspace_iff.mp (hT.hasEigenvector_eigenvectorBasis hn i).1

Premises used: Module.End.mem_eigenspace_iff, And.left, Iff.mp, LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
v : E
i : Fin n
this :
  ∀ (w : EuclideanSpace 𝕜 (Fin n)),
    Eq (α := E)
      ((T : (a : E) → E) (((hT.eigenvectorBasis hn).repr.symm : (a : EuclideanSpace 𝕜 (Fin n)) → E) w : E) : E)
      (((hT.eigenvectorBasis hn).repr.symm : (a : EuclideanSpace 𝕜 (Fin n)) → E)
          (toLp 2 fun (i : Fin n) ↦ (↑(hT.eigenvalues hn i) : (fun (x : Fin n) ↦ 𝕜) i) * w.ofLp i) :
        E)
⊢ ofLp (p := 2) (((hT.eigenvectorBasis hn).repr : (a : E) → EuclideanSpace 𝕜 (Fin n)) ((T : (a : E) → E) v)) i =
    HMul.hMul (α := (fun (x : Fin n) ↦ 𝕜) i) (↑(hT.eigenvalues hn i) : (fun (x : Fin n) ↦ 𝕜) i)
      (ofLp (p := 2) (((hT.eigenvectorBasis hn).repr : (a : E) → EuclideanSpace 𝕜 (Fin n)) v) i)

Tactic:
simpa [OrthonormalBasis.sum_repr_symm] using
      congr_arg (fun v => (hT.eigenvectorBasis hn).repr v i)
        (this ((hT.eigenvectorBasis hn).repr v))

Premises used: OrthonormalBasis.repr, congr_arg, LinearMap.IsSymmetric.eigenvectorBasis, OrthonormalBasis.sum_repr_symm, WithLp.ofLp, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
v : E
i : Fin n
w :
  ∀ (w : EuclideanSpace 𝕜 (Fin n)),
    Eq (α := E)
      ((T : (a : E) → E) (((hT.eigenvectorBasis hn).repr.symm : (a : EuclideanSpace 𝕜 (Fin n)) → E) w : E) : E)
      (((hT.eigenvectorBasis hn).repr.symm : (a : EuclideanSpace 𝕜 (Fin n)) → E)
          (toLp 2 fun (i : Fin n) ↦ (↑(hT.eigenvalues hn i) : (fun (x : Fin n) ↦ 𝕜) i) * w.ofLp i) :
        E)
⊢ ofLp (p := 2) (((hT.eigenvectorBasis hn).repr : (a : E) → EuclideanSpace 𝕜 (Fin n)) ((T : (a : E) → E) v)) i =
    HMul.hMul (α := (fun (x : Fin n) ↦ 𝕜) i) (↑(hT.eigenvalues hn i) : (fun (x : Fin n) ↦ 𝕜) i)
      (ofLp (p := 2) (((hT.eigenvectorBasis hn).repr : (a : E) → EuclideanSpace 𝕜 (Fin n)) v) i)

Tactic:
suffices
    ∀ w : EuclideanSpace 𝕜 (Fin n),
      T ((hT.eigenvectorBasis hn).repr.symm w) =
        (hT.eigenvectorBasis hn).repr.symm (toLp 2 fun i ↦ hT.eigenvalues hn i * w i) by
    simpa [OrthonormalBasis.sum_repr_symm] using
      congr_arg (fun v => (hT.eigenvectorBasis hn).repr v i)
        (this ((hT.eigenvectorBasis hn).repr v))
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
simp_rw :
  Eq.{u_2 + 1} (α := E)
    (∑ x : Fin n,
      w.ofLp x •
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑(hT.eigenvalues hn x) : 𝕜)
          ((hT.eigenvectorBasis hn : (a : Fin n) → E) x : E))
    (∑ x : Fin n,
      HSMul.hSMul (β := E) ((↑(hT.eigenvalues hn x) : 𝕜) * w.ofLp x) ((hT.eigenvectorBasis hn : (a : Fin n) → E) x : E))
⊢ Eq (α := E) ((T : (a : E) → E) (((hT.eigenvectorBasis hn).repr.symm : (a : EuclideanSpace 𝕜 (Fin n)) → E) w : E) : E)
    (((hT.eigenvectorBasis hn).repr.symm : (a : EuclideanSpace 𝕜 (Fin n)) → E)
        (toLp 2 fun (i : Fin n) ↦ (↑(hT.eigenvalues hn i) : (fun (x : Fin n) ↦ 𝕜) i) * w.ofLp i) :
      E)

Tactic:
simp_rw [← OrthonormalBasis.sum_repr_symm, map_sum, map_smul, apply_eigenvectorBasis]

Premises used: map_sum, OrthonormalBasis.sum_repr_symm, LinearMap.IsSymmetric.apply_eigenvectorBasis, map_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
h :
  ∀ (a : Fin n),
    w.ofLp a •
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑(hT.eigenvalues hn a) : 𝕜)
          ((hT.eigenvectorBasis hn : (a : Fin n) → E) a : E) =
      HSMul.hSMul (β := E) ((↑(hT.eigenvalues hn a) : 𝕜) * w.ofLp a) ((hT.eigenvectorBasis hn : (a : Fin n) → E) a : E)
⊢ Eq.{u_2 + 1} (α := E)
    (∑ x : Fin n,
      w.ofLp x •
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑(hT.eigenvalues hn x) : 𝕜)
          ((hT.eigenvectorBasis hn : (a : Fin n) → E) x : E))
    (∑ x : Fin n,
      HSMul.hSMul (β := E) ((↑(hT.eigenvalues hn x) : 𝕜) * w.ofLp x) ((hT.eigenvectorBasis hn : (a : Fin n) → E) x : E))

Tactic:
apply Fintype.sum_congr

Premises used: Fintype.sum_congr
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
a : Fin n
h :
  HSMul.hSMul (β := E) (w.ofLp a * (↑(hT.eigenvalues hn a) : 𝕜)) ((hT.eigenvectorBasis hn : (a : Fin n) → E) a : E) =
    HSMul.hSMul (β := E) ((↑(hT.eigenvalues hn a) : 𝕜) * w.ofLp a) ((hT.eigenvectorBasis hn : (a : Fin n) → E) a : E)
h₁ h₂ h₃ :
  HSMul.hSMul (β := E) ((↑(hT.eigenvalues hn a) : 𝕜) * w.ofLp a) ((hT.eigenvectorBasis hn : (a : Fin n) → E) a : E) =
    HSMul.hSMul (β := E) ((↑(hT.eigenvalues hn a) : 𝕜) * w.ofLp a) ((hT.eigenvectorBasis hn : (a : Fin n) → E) a : E)
⊢ w.ofLp a •
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑(hT.eigenvalues hn a) : 𝕜)
        ((hT.eigenvectorBasis hn : (a : Fin n) → E) a : E) =
    HSMul.hSMul (β := E) ((↑(hT.eigenvalues hn a) : 𝕜) * w.ofLp a) ((hT.eigenvectorBasis hn : (a : Fin n) → E) a : E)

Tactic:
rw [smul_smul, mul_comm, ofLp_toLp]

Premises used: smul_smul, mul_comm, WithLp.ofLp_toLp
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
a :
  ∀ (i j : Fin n),
    Eq.{u_1 + 1} (α := 𝕜)
      ((toMatrix (hT.eigenvectorBasis hn).toBasis (hT.eigenvectorBasis hn).toBasis :
            (a : E →ₗ[𝕜] E) → Matrix (Fin n) (Fin n) 𝕜)
          T i j :
        𝕜)
      (Matrix.diagonal (RCLike.ofReal ∘ hT.eigenvalues hn) i j : 𝕜)
⊢ Eq.{u_1 + 1} (α := Matrix (Fin n) (Fin n) 𝕜)
    ((toMatrix (hT.eigenvectorBasis hn).toBasis (hT.eigenvectorBasis hn).toBasis :
          (a : E →ₗ[𝕜] E) → Matrix (Fin n) (Fin n) 𝕜)
        T :
      Matrix (Fin n) (Fin n) 𝕜)
    (Matrix.diagonal (RCLike.ofReal ∘ hT.eigenvalues hn) : Matrix (Fin n) (Fin n) 𝕜)

Tactic:
ext i j