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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
v : E
μ : Eigenvalues T
w :
  ∀ (w : PiLp.{u_1, u_2} 2 fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ))),
    Eq (α := E)
      ((T : (a : E) → E)
          ((LinearIsometryEquiv.symm hT.diagonalization :
                (a : PiLp 2 fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ))) →
                  E)
              w :
            E) :
        E)
      ((LinearIsometryEquiv.symm hT.diagonalization :
            (a : PiLp 2 fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ))) → E)
          (toLp 2 fun (μ : Eigenvalues T) ↦ (↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ • w.ofLp μ) :
        E)
⊢ ofLp (p := 2)
      ((hT.diagonalization :
          (a : E) → PiLp 2 fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ)))
        ((T : (a : E) → E) v))
      μ =
    HSMul.hSMul (β := (fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ))) μ)
      ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ)
      (ofLp (p := 2)
        ((hT.diagonalization :
            (a : E) → PiLp 2 fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ)))
          v)
        μ)

Tactic:
suffices
    ∀ w : PiLp 2 fun μ : Eigenvalues T => eigenspace T μ,
      T (hT.diagonalization.symm w) = hT.diagonalization.symm (toLp 2 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))
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
v : E
μ : Eigenvalues T
w : PiLp.{u_1, u_2} 2 fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ))
⊢ ∀ (μ : Eigenvalues T),
    (T : (a : E) → E) (↑(w.ofLp μ) : E) = (↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ • (↑(w.ofLp μ) : E)

Tactic:
have hwT : ∀ μ, T (w μ) = (μ : 𝕜) • w μ := fun μ => mem_eigenspace_iff.1 (w μ).2
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
v : E
μ : Eigenvalues T
w : PiLp.{u_1, u_2} 2 fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ))
hwT :
  ∀ (μ : Eigenvalues T),
    (T : (a : E) → E) (↑(w.ofLp μ) : E) = (↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ • (↑(w.ofLp μ) : E)
⊢ Eq (α := E)
    ((T : (a : E) → E)
        ((LinearIsometryEquiv.symm hT.diagonalization :
              (a : PiLp 2 fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ))) →
                E)
            w :
          E) :
      E)
    ((LinearIsometryEquiv.symm hT.diagonalization :
          (a : PiLp 2 fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ))) → E)
        (toLp 2 fun (μ : Eigenvalues T) ↦ (↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ • w.ofLp μ) :
      E)

Tactic:
simp only [diagonalization_symm_apply, map_sum, hwT, SetLike.val_smul]

Premises used: LinearMap.IsSymmetric.diagonalization_symm_apply, map_sum, SetLike.val_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
i : Fin n
let :
  ∀ (x : 𝕜) (hx : HasUnifEigenvalue T x 1),
    HasEigenvalue T
      (↑((RCLike.re : (a : 𝕜) → ℝ)
            ((↑T : Eigenvalues T → 𝕜) (Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) x hx))) :
        𝕜)
⊢ HasEigenvalue T
    (↑((RCLike.re : (a : 𝕜) → ℝ)
          ((↑T : Eigenvalues T → 𝕜) (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯))) :
      𝕜)

Tactic:
let ⟨x, hx⟩ := hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
    hT.orthogonalFamily_eigenspaces'
-- 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
x : 𝕜
hx : HasUnifEigenvalue T x 1
rwa : HasEigenvalue T (↑((RCLike.re : (a : 𝕜) → ℝ) x) : 𝕜)
rwa₁ rwa₂ rwa₃ rwa₄ : HasEigenvalue T x
⊢ HasEigenvalue T
    (↑((RCLike.re : (a : 𝕜) → ℝ)
          ((↑T : Eigenvalues T → 𝕜) (Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) x hx))) :
      𝕜)

Tactic:
rwa [Eigenvalues.val_mk, RCLike.conj_eq_iff_re.mp (hT.conj_eigenvalue_eq_self hx)]

Premises used: LinearMap.IsSymmetric.conj_eigenvalue_eq_self, RCLike.conj_eq_iff_re, Iff.mp, Module.End.Eigenvalues.val_mk
-- 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 μ
⊢ let x := Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ;
  x = Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ

Tactic:
let (eq := hx) x : Eigenvalues T := ⟨μ, 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
μ : 𝕜
hμ : HasEigenvalue T μ
x : Eigenvalues T := Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ
hx : x = Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ
obtain :
  ∀ (i : Fin n) (hi : DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯ = x),
    ∃ (i : Fin n), (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ
⊢ ∃ (i : Fin n), (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ

Tactic:
obtain ⟨i, hi⟩ := hT.direct_sum_isInternal.exists_subordinateOrthonormalBasisIndex_eq hn
    hT.orthogonalFamily_eigenspaces' (hasEigenvalue_iff.mp x.prop)

Premises used: DirectSum.IsInternal.exists_subordinateOrthonormalBasisIndex_eq, Module.End.hasEigenvalue_iff, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', LinearMap.IsSymmetric.direct_sum_isInternal, Subtype.prop, Iff.mp
-- 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 μ
x : Eigenvalues T := Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ
hx : x = Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ
i : Fin n
hi : DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯ = x
h : (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ
⊢ ∃ (i : Fin n), (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ

Tactic:
use i
-- 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 μ
x : Eigenvalues T := Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ
hx : x = Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ
i : Fin n
hi : DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯ = x
h :
  (↑((RCLike.re : (a : 𝕜) → ℝ)
          ((↑T : Eigenvalues T → 𝕜) (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯))) :
      𝕜) =
    μ
h₁ : (↑((RCLike.re : (a : 𝕜) → ℝ) ((↑T : Eigenvalues T → 𝕜) x)) : 𝕜) = μ
h₂ :
  (↑((RCLike.re : (a : 𝕜) → ℝ)
          ((↑T : Eigenvalues T → 𝕜) (Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ))) :
      𝕜) =
    μ
h₃ : (↑((RCLike.re : (a : 𝕜) → ℝ) μ) : 𝕜) = μ
h₄ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ
h₅ h₆ : μ = μ
⊢ (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ

Tactic:
rw [unsortedEigenvalues, hi, hx, Eigenvalues.val_mk, ← RCLike.conj_eq_iff_re,
    hT.conj_eigenvalue_eq_self hμ]

Premises used: LinearMap.IsSymmetric.conj_eigenvalue_eq_self, RCLike.conj_eq_iff_re, Module.End.Eigenvalues.val_mk, _private.0.LinearMap.IsSymmetric.unsortedEigenvalues
-- 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
μ : 𝕜
pos :
  ∀ (hμ : HasEigenvalue T μ),
    Finset.card (α := Fin n) {i : Fin n | (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ} =
      finrank.{u_1, u_2} 𝕜 ↥(eigenspace T μ)
neg :
  ∀ (hμ : ¬HasEigenvalue T μ),
    Finset.card (α := Fin n) {i : Fin n | (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ} =
      finrank.{u_1, u_2} 𝕜 ↥(eigenspace T μ)
⊢ Finset.card (α := Fin n) {i : Fin n | (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ} =
    finrank.{u_1, u_2} 𝕜 ↥(eigenspace T μ)

Tactic:
by_cases hμ : HasEigenvalue T μ

Premises used: Module.End.HasEigenvalue
-- 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 μ
⊢ Finset.card (α := Fin n)
      {a : Fin n |
        DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ a ⋯ =
          Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ} =
    finrank.{u_1, u_2} 𝕜
      ↥(eigenspace T
          ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 (Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ)))

Tactic:
hT.direct_sum_isInternal.card_filter_subordinateOrthonormalBasisIndex_eq hn
        hT.orthogonalFamily_eigenspaces' ⟨μ, hμ⟩

Premises used: LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', Subtype.mk, LinearMap.IsSymmetric.direct_sum_isInternal, DirectSum.IsInternal.card_filter_subordinateOrthonormalBasisIndex_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 μ
h :
  ∀ (i : Fin n),
    Membership.mem (γ := Finset (Fin n)) Finset.univ i →
      ((↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ ↔
        DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯ =
          Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ)
⊢ Finset.card (α := Fin n) {i : Fin n | (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ} =
    finrank.{u_1, u_2} 𝕜 ↥(eigenspace T μ)

Tactic:
convert!
      hT.direct_sum_isInternal.card_filter_subordinateOrthonormalBasisIndex_eq hn
        hT.orthogonalFamily_eigenspaces' ⟨μ, hμ⟩ with i

Premises used: LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', Subtype.mk, LinearMap.IsSymmetric.direct_sum_isInternal, DirectSum.IsInternal.card_filter_subordinateOrthonormalBasisIndex_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
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ i
h :
  ∀ (x : 𝕜) (hx : HasUnifEigenvalue T x 1),
    (↑((RCLike.re : (a : 𝕜) → ℝ)
              ((↑T : Eigenvalues T → 𝕜) (Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) x hx))) :
          𝕜) =
        μ ↔
      Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) x hx =
        Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ)
            ((↑T : Eigenvalues T → 𝕜) (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯))) :
        𝕜) =
      μ ↔
    DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯ =
      Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ

Tactic:
let ⟨x, hx⟩ := hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
      hT.orthogonalFamily_eigenspaces'
-- 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
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ i
x : 𝕜
hx : HasUnifEigenvalue T x 1
h :
  x = μ ↔
    Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) x hx =
      Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ
⊢ (↑((RCLike.re : (a : 𝕜) → ℝ)
            ((↑T : Eigenvalues T → 𝕜) (Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) x hx))) :
        𝕜) =
      μ ↔
    Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) x hx =
      Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ

Tactic:
rw [Eigenvalues.val_mk, RCLike.conj_eq_iff_re.mp (hT.conj_eigenvalue_eq_self hx)]

Premises used: LinearMap.IsSymmetric.conj_eigenvalue_eq_self, RCLike.conj_eq_iff_re, Iff.mp, Module.End.Eigenvalues.val_mk
-- 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
h : Membership.mem (γ := Finset (Fin n)) Finset.univ i
x : 𝕜
hx : HasUnifEigenvalue T x 1
⊢ x = μ ↔
    Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) x hx =
      Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ

Tactic:
Subtype.mk_eq_mk.symm

Premises used: Subtype.mk_eq_mk, Module.End.UnifEigenvalues, Iff.symm
-- 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
h : Membership.mem (γ := Finset (Fin n)) Finset.univ i
x : 𝕜
hx : HasUnifEigenvalue T x 1
⊢ x = μ ↔
    Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) x hx =
      Subtype.mk (p := fun (μ : 𝕜) ↦ HasUnifEigenvalue T μ 1) μ hμ

Tactic:
exact Subtype.mk_eq_mk.symm

Premises used: Subtype.mk_eq_mk, Iff.symm
-- 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 μ
neg : ∀ (x : Fin n), Membership.mem (γ := Finset (Fin n)) Finset.univ x → ¬(↑(hT.unsortedEigenvalues hn x) : 𝕜) = μ
⊢ Finset.card (α := Fin n) {i : Fin n | (↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ} =
    finrank.{u_1, u_2} 𝕜 ↥(eigenspace T μ)

Tactic:
rw [Module.End.hasEigenvalue_iff.not_left.mp hμ, finrank_bot, Finset.card_filter_eq_zero_iff]

Premises used: Module.End.hasEigenvalue_iff, Finset.card_filter_eq_zero_iff, Iff.not_left, Iff.mp, finrank_bot
-- 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
neg : Membership.mem (γ := Finset (Fin n)) Finset.univ i → ¬(↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ
⊢ Membership.mem (γ := Finset (Fin n)) Finset.univ i → ¬(↑(hT.unsortedEigenvalues hn i) : 𝕜) = μ

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
i : Fin n
h : Membership.mem (γ := Finset (Fin n)) Finset.univ i
hμ : ¬HasEigenvalue T (↑(hT.unsortedEigenvalues hn i) : 𝕜)
⊢ False

Tactic:
hμ (hT.hasEigenvalue_unsortedEigenvalues hn i)

Premises used: _private.0.LinearMap.IsSymmetric.hasEigenvalue_unsortedEigenvalues
-- 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
h : Membership.mem (γ := Finset (Fin n)) Finset.univ i
hμ : ¬HasEigenvalue T (↑(hT.unsortedEigenvalues hn i) : 𝕜)
⊢ False

Tactic:
exact hμ (hT.hasEigenvalue_unsortedEigenvalues hn i)

Premises used: _private.0.LinearMap.IsSymmetric.hasEigenvalue_unsortedEigenvalues
-- 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 ⋯)
change : HasEigenvector T (↑((RCLike.re : (a : 𝕜) → ℝ) μ) : 𝕜) v
⊢ HasEigenvector T
    (↑((RCLike.re : (a : 𝕜) → ℝ)
          ((↑T : Eigenvalues T → 𝕜) (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯))) :
      𝕜)
    ((hT.unsortedEigenvectorBasis hn : (a : Fin n) → E) i)

Tactic:
change HasEigenvector T (RCLike.re μ) v

Premises used: Module.End.HasEigenvector, RCLike.ofReal, RCLike.re, 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
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn : (a : Fin n) → E) i
μ : 𝕜 := (↑T : Eigenvalues T → 𝕜) (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
simp_rw :
  Membership.mem (α := E) (eigenspace T μ)
    ((DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯ : (a : Fin n) → E) i : E)
⊢ v ∈ eigenspace T μ

Tactic:
simp_rw [v, unsortedEigenvectorBasis]

Premises used: _private.0.LinearMap.IsSymmetric.unsortedEigenvectorBasis
-- 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 ⋯)
⊢ Membership.mem (α := E) (eigenspace T μ)
    ((DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯ : (a : Fin n) → E) i : E)

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

Premises used: Set.Mem, DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate, setOf, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', LinearMap.IsSymmetric.direct_sum_isInternal
-- 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 ⋯)
⊢ Membership.mem (α := E) (eigenspace T μ)
    ((DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯ : (a : Fin n) → E) i : E)

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

Premises used: DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', LinearMap.IsSymmetric.direct_sum_isInternal
-- 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 ⋯)
⊢ v ∈ eigenspace T μ

Tactic:
have H₁ : v ∈ eigenspace T μ := by
      simp_rw [v, unsortedEigenvectorBasis]
      exact
        hT.direct_sum_isInternal.subordinateOrthonormalBasis_subordinate hn i
          hT.orthogonalFamily_eigenspaces'
-- 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 ⋯)
H₁ : v ∈ eigenspace T μ
⊢ v ≠ 0

Tactic:
simpa using (hT.unsortedEigenvectorBasis hn).toBasis.ne_zero i

Premises used: Module.Basis.ne_zero, _private.0.LinearMap.IsSymmetric.unsortedEigenvectorBasis, OrthonormalBasis.toBasis
-- 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 ⋯)
H₁ : v ∈ eigenspace T μ
⊢ v ≠ 0

Tactic:
have H₂ : v ≠ 0 := by simpa using (hT.unsortedEigenvectorBasis hn).toBasis.ne_zero i
-- 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 ⋯)
H₁ : v ∈ eigenspace T μ
H₂ : v ≠ 0
⊢ HasEigenvector T μ v

Tactic:
⟨H₁, H₂⟩

Premises used: Module.End.HasUnifEigenvector, And.intro
-- 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 ⋯)
H₁ : v ∈ eigenspace T μ
H₂ : v ≠ 0
⊢ HasEigenvector T μ v

Tactic:
exact ⟨H₁, H₂⟩