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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
this : (T : (a : E) → E) w = μ • w
⊢ ⟪w, (T : (a : E) → E) v⟫ = 0

Tactic:
simp [← hT w, this, inner_smul_left, hv w hw]

Premises used: inner_smul_left
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
hμ : HasEigenvalue T μ
obtain :
  ∀ (v : E)
    (hv₁ : Membership.mem (γ := Submodule 𝕜 E) ((genEigenspace T μ : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) v)
    (hv₂ : v ≠ 0), (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ

Tactic:
obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector

Premises used: Module.End.HasEigenvalue.exists_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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : Membership.mem (γ := Submodule 𝕜 E) ((genEigenspace T μ : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) v
hv₂ : v ≠ 0
⊢ (T : (a : E) → E) v = μ • v

Tactic:
rw [mem_eigenspace_iff] at hv₁

Premises used: Module.End.mem_eigenspace_iff
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : Membership.mem (γ := Submodule 𝕜 E) ((genEigenspace T μ : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) v
hv₂ : v ≠ 0
hv₃ : (T : (a : E) → E) v = μ • v
⊢ v ≠ 0

Tactic:
rw [mem_eigenspace_iff] at hv₁

Premises used: Module.End.mem_eigenspace_iff
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : (T : (a : E) → E) v = μ • v
hv₂ : v ≠ 0
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ

Tactic:
simpa [hv₂, inner_smul_left, inner_smul_right, hv₁] using hT v v

Premises used: inner_smul_right, inner_smul_left
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
pos :
  ∀ (hv' : v = 0),
    inner 𝕜 (E := E)
        (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) μ : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) μ) → E)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T μ) v hv) :
          E)
        (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) ν : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) ν) → E)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T ν) w hw) :
          E) =
      0
neg :
  ∀ (hv' : ¬v = 0),
    inner 𝕜 (E := E)
        (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) μ : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) μ) → E)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T μ) v hv) :
          E)
        (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) ν : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) ν) → E)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T ν) w hw) :
          E) =
      0
⊢ inner 𝕜 (E := E)
      (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) μ : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) μ) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T μ) v hv) :
        E)
      (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) ν : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) ν) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T ν) w hw) :
        E) =
    0

Tactic:
by_cases hv' : v = 0
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : v = 0
⊢ inner 𝕜 (E := E)
      (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) μ : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) μ) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T μ) v hv) :
        E)
      (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) ν : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) ν) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T ν) w hw) :
        E) =
    0

Tactic:
simp [hv']
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : ¬v = 0
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ

Tactic:
have H := hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector ⟨hv, hv'⟩)
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : ¬v = 0
H : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ
neg :
  ∀ (hv_1 : (T : (a : E) → E) v = μ • v) (w : E) (hw : w ∈ eigenspace T ν) (hw_1 : (T : (a : E) → E) w = ν • w)
    (hv' : ¬v = 0) (H : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ),
    inner 𝕜 (E := E)
        (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) μ : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) μ) → E)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T μ) v hv) :
          E)
        (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) ν : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) ν) → E)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T ν) w hw) :
          E) =
      0
⊢ inner 𝕜 (E := E)
      (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) μ : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) μ) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T μ) v hv) :
        E)
      (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) ν : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) ν) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T ν) w hw) :
        E) =
    0

Tactic:
rw [mem_eigenspace_iff] at hv hw

Premises used: Module.End.mem_eigenspace_iff
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv_1 : v ∈ eigenspace T μ
hv : (T : (a : E) → E) v = μ • v
w : E
hw_1 : w ∈ eigenspace T ν
hw : (T : (a : E) → E) w = ν • w
hv' : ¬v = 0
H : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ
⊢ inner 𝕜 (E := E)
      (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) μ : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) μ) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T μ) v hv_1) :
        E)
      (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) ν : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) ν) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T ν) w hw_1) :
        E) =
    0

Tactic:
Or.resolve_left ?_ hμν.symm

Premises used: Or.resolve_left, Ne.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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv_1 : v ∈ eigenspace T μ
hv : (T : (a : E) → E) v = μ • v
w : E
hw_1 : w ∈ eigenspace T ν
hw : (T : (a : E) → E) w = ν • w
hv' : ¬v = 0
H : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ
neg :
  ν = μ ∨
    inner 𝕜 (E := E)
        (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) μ : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) μ) → E)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T μ) v hv_1) :
          E)
        (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) ν : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) ν) → E)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T ν) w hw_1) :
          E) =
      0
⊢ inner 𝕜 (E := E)
      (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) μ : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) μ) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T μ) v hv_1) :
        E)
      (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) ν : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) ν) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T ν) w hw_1) :
        E) =
    0

Tactic:
refine Or.resolve_left ?_ hμν.symm

Premises used: Or.resolve_left, Ne.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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv_1 : v ∈ eigenspace T μ
hv : (T : (a : E) → E) v = μ • v
w : E
hw_1 : w ∈ eigenspace T ν
hw : (T : (a : E) → E) w = ν • w
hv' : ¬v = 0
H : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ
⊢ ν = μ ∨
    inner 𝕜 (E := E)
        (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) μ : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) μ) → E)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T μ) v hv_1) :
          E)
        (((fun (μ : 𝕜) ↦ (eigenspace T μ).subtypeₗᵢ) ν : (a : (fun (μ : 𝕜) ↦ ↥(eigenspace T μ)) ν) → E)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ eigenspace T ν) w hw_1) :
          E) =
      0

Tactic:
simpa [inner_smul_left, inner_smul_right, hv, hw, H] using (hT v w).symm

Premises used: inner_smul_right, Eq.symm, inner_smul_left
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ OrthogonalFamily.{u_1, u_2, u_1, u_2} 𝕜 (E := E)
    (fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ)))
    fun (μ : Eigenvalues T) ↦ (eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ)).subtypeₗᵢ

Tactic:
hT.orthogonalFamily_eigenspaces.comp Subtype.coe_injective

Premises used: LinearMap.IsSymmetric.orthogonalFamily_eigenspaces, Set.Mem, Subtype.coe_injective, OrthogonalFamily.comp
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
v : E
hv : Membership.mem (γ := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ v
rw :
  ∀ (hv : Membership.mem (γ := Submodule 𝕜 E) (⨅ (i : 𝕜), (eigenspace T i)ᗮ) v),
    Membership.mem (α := E) (γ := Submodule 𝕜 E) (⨅ (i : 𝕜), (eigenspace T i)ᗮ) ((T : (a : E) → E) v : E)
⊢ Membership.mem (α := E) (γ := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ ((T : (a : E) → E) v : E)

Tactic:
rw [← Submodule.iInf_orthogonal] at hv ⊢

Premises used: Submodule.iInf_orthogonal
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
v : E
hv : Membership.mem (γ := Submodule 𝕜 E) (⨅ (i : 𝕜), (eigenspace T i)ᗮ) v
⊢ Membership.mem (α := E) (γ := Submodule 𝕜 E) (⨅ (i : 𝕜), (eigenspace T i)ᗮ) ((T : (a : E) → E) v : E)

Tactic:
T.iInf_invariant hT.invariant_orthogonalComplement_eigenspace v hv

Premises used: LinearMap.iInf_invariant, LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
v : E
hv : Membership.mem (γ := Submodule 𝕜 E) (⨅ (i : 𝕜), (eigenspace T i)ᗮ) v
⊢ Membership.mem (α := E) (γ := Submodule 𝕜 E) (⨅ (i : 𝕜), (eigenspace T i)ᗮ) ((T : (a : E) → E) v : E)

Tactic:
exact T.iInf_invariant hT.invariant_orthogonalComplement_eigenspace v hv

Premises used: LinearMap.iInf_invariant, LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ eigenspace (T.restrict ⋯) μ = ⊥

Tactic:
eigenspace_restrict_eq_bot hT.orthogonalComplement_iSup_eigenspaces_invariant ?_

Premises used: Set.Mem, setOf, Module.End.eigenspace_restrict_eq_bot, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
refine : Disjoint (eigenspace T μ) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ eigenspace (T.restrict ⋯) μ = ⊥

Tactic:
refine eigenspace_restrict_eq_bot hT.orthogonalComplement_iSup_eigenspaces_invariant ?_

Premises used: Module.End.eigenspace_restrict_eq_bot, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ eigenspace T μ ⟂ p

Tactic:
have H₂ : eigenspace T μ ⟂ p := (Submodule.isOrtho_orthogonal_right _).mono_left (le_iSup _ _)
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
H₂ : eigenspace T μ ⟂ p
⊢ Disjoint (eigenspace T μ) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ

Tactic:
H₂.disjoint

Premises used: Set.Mem, setOf, Submodule.IsOrtho.disjoint
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
H₂ : eigenspace T μ ⟂ p
⊢ Disjoint (eigenspace T μ) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ

Tactic:
exact H₂.disjoint

Premises used: Submodule.IsOrtho.disjoint
-- 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
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := ↥(⨆ (μ : 𝕜), eigenspace T μ)ᗮ) (T.restrict ⋯)

Tactic:
have hT' : IsSymmetric _ :=
    hT.restrict_invariant hT.orthogonalComplement_iSup_eigenspaces_invariant
-- 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
hT' : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := ↥(⨆ (μ : 𝕜), eigenspace T μ)ᗮ) (T.restrict ⋯)
⊢ Subsingleton.{u_2 + 1} ↥(⨆ (μ : 𝕜), eigenspace T μ)ᗮ

Tactic:
haveI :=
    hT'.subsingleton_of_no_eigenvalue_finiteDimensional hT.orthogonalComplement_iSup_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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hT' : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := ↥(⨆ (μ : 𝕜), eigenspace T μ)ᗮ) (T.restrict ⋯)
this : Subsingleton.{u_2 + 1} ↥(⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ ⊥

Tactic:
Submodule.eq_bot_of_subsingleton

Premises used: Submodule.eq_bot_of_subsingleton
-- 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
hT' : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := ↥(⨆ (μ : 𝕜), eigenspace T μ)ᗮ) (T.restrict ⋯)
this : Subsingleton.{u_2 + 1} ↥(⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ ⊥

Tactic:
exact Submodule.eq_bot_of_subsingleton

Premises used: Submodule.eq_bot_of_subsingleton
-- 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
rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (i : 𝕜), eigenspace T i)ᗮ ⊥
rw₁ rw₂ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ ⊥
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : { μ : 𝕜 // eigenspace T μ ≠ ⊥ }), eigenspace T (↑μ : 𝕜))ᗮ ⊥

Tactic:
rw [iSup_ne_bot_subtype, hT.orthogonalComplement_iSup_eigenspaces_eq_bot]

Premises used: LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot, iSup_ne_bot_subtype
-- 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 : Fact (IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T)
μ : Eigenvalues T
⊢ CompleteSpace.{u_2} ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ))

Tactic:
infer_instance
-- 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 : Fact (IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T)
x : E
μ : Eigenvalues T
⊢ (((DirectSum.decompose fun (μ : Eigenvalues T) ↦ eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ) :
              (a : E) →
                DirectSum (Eigenvalues T) fun (i : Eigenvalues T) ↦
                  ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 i)))
            x :
          DirectSum.{u_1, u_2} (Eigenvalues T) fun (i : Eigenvalues T) ↦
            ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 i))) :
        (a : Eigenvalues T) → ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 a)))
      μ =
    ((eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ)).orthogonalProjection :
        (a : E) → ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ)))
      x

Tactic:
rfl

Premises used: Set.Mem, rfl
-- 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
⊢ DirectSum.IsInternal (S := Submodule 𝕜 E) fun (μ : Eigenvalues T) ↦
    eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ)

Tactic:
hT.orthogonalFamily_eigenspaces'.isInternal_iff.mpr
    hT.orthogonalComplement_iSup_eigenspaces_eq_bot'

Premises used: Iff.mpr, OrthogonalFamily.isInternal_iff, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
w : PiLp.{u_1, u_2} 2 fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ))
⊢ Eq.{u_2 + 1} (α := E)
    ((LinearIsometryEquiv.symm hT.diagonalization :
          (a : PiLp 2 fun (μ : Eigenvalues T) ↦ ↥(eigenspace T ((↑T : (k : ℕ∞) → UnifEigenvalues T k → 𝕜) 1 μ))) → E)
        w :
      E)
    (∑ μ : Eigenvalues T, (↑(w.ofLp μ) : E) : E)

Tactic:
hT.direct_sum_isInternal.isometryL2OfOrthogonalFamily_symm_apply
    hT.orthogonalFamily_eigenspaces' w

Premises used: DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply, 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
v : E
μ : Eigenvalues T
this :
  ∀ (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:
simpa only [LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.apply_symm_apply] using
      congr_arg (fun w => hT.diagonalization w μ) (this (hT.diagonalization v))

Premises used: LinearMap.IsSymmetric.diagonalization, LinearIsometryEquiv.apply_symm_apply, congr_arg, LinearIsometryEquiv.symm_apply_apply, WithLp.ofLp, DFunLike.coe