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
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
hT' : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
push :
  (∃ (μ : 𝕜), HasEigenvalue (↑T : E →ₗ[𝕜] E) μ ∧ μ ≠ 0) ↔
    ∃ (i : 𝕜), Ne (α := ENNReal) (⨆ (_ : i ∈ spectrum 𝕜 T), (↑‖i‖₊ : ENNReal)) 0
⊢ (¬∀ (μ : 𝕜), HasEigenvalue (↑T : E →ₗ[𝕜] E) μ → μ = 0) ↔
    ¬∀ (i : 𝕜), Eq (α := ENNReal) (⨆ (_ : i ∈ spectrum 𝕜 T), (↑‖i‖₊ : ENNReal)) 0

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
hT' : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
h :
  ∀ (a : 𝕜),
    HasEigenvalue (↑T : E →ₗ[𝕜] E) a ∧ a ≠ 0 ↔ Ne (α := ENNReal) (⨆ (_ : a ∈ spectrum 𝕜 T), (↑‖a‖₊ : ENNReal)) 0
⊢ (∃ (μ : 𝕜), HasEigenvalue (↑T : E →ₗ[𝕜] E) μ ∧ μ ≠ 0) ↔
    ∃ (i : 𝕜), Ne (α := ENNReal) (⨆ (_ : i ∈ spectrum 𝕜 T), (↑‖i‖₊ : ENNReal)) 0

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
hT' : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
⊢ ∀ (a : 𝕜),
    HasEigenvalue (↑T : E →ₗ[𝕜] E) a ∧ a ≠ 0 ↔ Ne (α := ENNReal) (⨆ (_ : a ∈ spectrum 𝕜 T), (↑‖a‖₊ : ENNReal)) 0

Tactic:
simp +contextual [hT.hasEigenvalue_iff_mem_spectrum]

Premises used: IsCompactOperator.hasEigenvalue_iff_mem_spectrum
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
hT' : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →L[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ := T.restrict ⋯
⊢ IsCompactOperator (M₁ := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) (M₂ :=
    ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (⇑S : (a : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) → ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)

Tactic:
have hS_compact : IsCompactOperator S :=
    hT.restrict' 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
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
hT' : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →L[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ := T.restrict ⋯
hS_compact :
  IsCompactOperator (M₁ := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) (M₂ :=
    ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (⇑S : (a : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) → ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
⊢ LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)

Tactic:
have hS_symm : S.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
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
hT' : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →L[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ := T.restrict ⋯
hS_compact :
  IsCompactOperator (M₁ := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) (M₂ :=
    ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (⇑S : (a : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) → ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS_symm :
  LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
⊢ ∀ (μ : 𝕜),
    eigenspace (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
        μ =
      ⊥

Tactic:
have hS μ : eigenspace (S : Module.End 𝕜 (⨆ μ, eigenspace T μ : Submodule 𝕜 E)ᗮ) μ = ⊥ :=
    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
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
hT' : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →L[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ := T.restrict ⋯
hS_compact :
  IsCompactOperator (M₁ := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) (M₂ :=
    ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (⇑S : (a : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) → ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS_symm :
  LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS :
  ∀ (μ : 𝕜),
    eigenspace (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
        μ =
      ⊥
μ : 𝕜
⊢ HasEigenvalue (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
      μ →
    μ = 0

Tactic:
simp_all [hasEigenvalue_iff]

Premises used: Module.End.hasEigenvalue_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
hT' : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →L[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ := T.restrict ⋯
hS_compact :
  IsCompactOperator (M₁ := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) (M₂ :=
    ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (⇑S : (a : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) → ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS_symm :
  LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS :
  ∀ (μ : 𝕜),
    eigenspace (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
        μ =
      ⊥
⊢ ∀ (μ : 𝕜),
    HasEigenvalue (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
        μ →
      μ = 0

Tactic:
have h μ : HasEigenvalue (S : End 𝕜 (⨆ μ, eigenspace T μ : Submodule 𝕜 E)ᗮ) μ → μ = 0 := by
    simp_all [hasEigenvalue_iff]
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
hT' : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →L[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ := T.restrict ⋯
hS_compact :
  IsCompactOperator (M₁ := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) (M₂ :=
    ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (⇑S : (a : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) → ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS_symm :
  LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS :
  ∀ (μ : 𝕜),
    eigenspace (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
        μ =
      ⊥
h :
  ∀ (μ : 𝕜),
    HasEigenvalue (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
        μ →
      μ = 0
⊢ S = 0

Tactic:
rw [eq_zero_of_forall_hasEigenvalue_eq_zero hS_compact hS_symm] at h

Premises used: ContinuousLinearMap.eq_zero_of_forall_hasEigenvalue_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
hT' : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →L[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ := T.restrict ⋯
hS_compact :
  IsCompactOperator (M₁ := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) (M₂ :=
    ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (⇑S : (a : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) → ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS_symm :
  LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS :
  ∀ (μ : 𝕜),
    eigenspace (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
        μ =
      ⊥
h : S = 0
rw : Subsingleton.{u_2 + 1} ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ ⊥

Tactic:
rw [← Submodule.subsingleton_iff_eq_bot]

Premises used: Submodule.subsingleton_iff_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
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
hT' : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →L[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ := T.restrict ⋯
hS_compact :
  IsCompactOperator (M₁ := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) (M₂ :=
    ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (⇑S : (a : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) → ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS_symm :
  LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS :
  ∀ (μ : 𝕜),
    eigenspace (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
        μ =
      ⊥
h : S = 0
by_contra! : ∀ (hV : Nontrivial.{u_2} ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ), False
⊢ Subsingleton.{u_2 + 1} ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ

Tactic:
by_contra! hV
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
hT' : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →L[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ := T.restrict ⋯
hS_compact :
  IsCompactOperator (M₁ := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) (M₂ :=
    ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (⇑S : (a : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ) → ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS_symm :
  LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
    (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
hS :
  ∀ (μ : 𝕜),
    eigenspace (↑S : ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ →ₗ[𝕜] ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ)
        μ =
      ⊥
h : S = 0
hV : Nontrivial.{u_2} ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ
⊢ False

Tactic:
simpa [h] using hS 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator (M₁ := E) (M₂ := E) (⇑T : (a : E) → E)
μ : 𝕜
hμ : μ ≠ 0
⊢ IsCompactOperator (M₁ := ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)) (M₂ := ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ))
    (⇑((↑T : E →ₗ[𝕜] E).restrict ⋯) : (a : ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)) → ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ))

Tactic:
replace hT := hT.restrict'
    ((mem_invtSubmodule_iff_forall_mem_of_mem _).mp (eigenspace_mem_invtSubmodule T.toLinearMap μ))
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
μ : 𝕜
hμ : μ ≠ 0
hT :
  IsCompactOperator (M₁ := ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)) (M₂ := ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ))
    (⇑((↑T : E →ₗ[𝕜] E).restrict ⋯) : (a : ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)) → ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ))
⊢ IsCompactOperator.{u_2, u_2} (M₁ := ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)) (M₂ := ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ))
    (⇑LinearMap.id : (a : ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)) → ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ))

Tactic:
rw [restrict_eigenspace, LinearMap.coe_smul, IsCompactOperator.smul_iff₀ hμ] at hT

Premises used: LinearMap.coe_smul, Module.End.restrict_eigenspace, IsCompactOperator.smul_iff₀
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
μ : 𝕜
hμ : μ ≠ 0
hT :
  IsCompactOperator.{u_2, u_2} (M₁ := ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)) (M₂ := ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ))
    (⇑LinearMap.id : (a : ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)) → ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ))
rwa rwa₁ rwa₂ rwa₃ : IsCompactOperator.{u_2, u_2} (M₁ := ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)) id
⊢ FiniteDimensional.{u_1, u_2} 𝕜 ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)

Tactic:
rwa [← isCompactOperator_id_iff_finiteDimensional]

Premises used: isCompactOperator_id_iff_finiteDimensional
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
c : ℂˣ
x : H
⊢ (scalarSMulCLE H c : (a : H) → H) x = c • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
c : ℂˣ
x : H
⊢ (ContinuousLinearEquiv.symm (scalarSMulCLE H c) : (a : H) → H) x = c⁻¹ • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
⊢ ∀ (x : H), HPow.hPow (β := ℕ) ‖x‖ 2 = (RCLike.re : (a : ℝ) → ℝ) ⟪x, x⟫.re

Tactic:
simp [RCLike.re_to_real, ipc.norm_sq_eq_re_inner]

Premises used: RCLike.re_to_real, InnerProductSpace.norm_sq_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x y : H
simp : ⟪y, x⟫.re = re ((starRingEnd ℂ : (a : ℂ) → ℂ) ⟪y, x⟫)
⊢ (starRingEnd ℝ : (a : ℝ) → ℝ) ⟪y, x⟫.re = ⟪x, y⟫.re

Tactic:
simp only [← ipc.conj_inner_symm x y, conj_trivial]

Premises used: conj_trivial, InnerProductSpace.conj_inner_symm
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x y : H
⊢ ⟪y, x⟫.re = re ((starRingEnd ℂ : (a : ℂ) → ℂ) ⟪y, x⟫)

Tactic:
rfl
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
⊢ ∀ (x y z : H), ⟪x + y, z⟫.re = ⟪x, z⟫.re + ⟪y, z⟫.re

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
⊢ ∀ (x y : H) (r : ℝ), ⟪r • x, y⟫.re = HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪x, y⟫.re

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x y : H
⊢ inner ℝ x y = ⟪x, y⟫.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
⊢ I * -I = 1

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
⊢ -I * I = 1

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ S ↔ x ∈ (↑S : Submodule ℝ H).carrier

Tactic:
Eq.to_iff rfl

Premises used: Eq.to_iff, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ S ↔ x ∈ (↑S : Submodule ℝ H).carrier

Tactic:
exact Eq.to_iff rfl

Premises used: Eq.to_iff, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
simp : (∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0) ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0
⊢ x ∈ S.symplComp ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0

Tactic:
simp only [mem_orthogonal, mem_mapEquiv_iff, scalarSMulCLE_symm_apply, Units.smul_def,
    Units.val_inv_eq_inv_val, val_UnitI, inv_I, neg_smul]

Premises used: Complex.inv_I, neg_smul, Complex.val_UnitI, scalarSMulCLE_symm_apply, Units.val_inv_eq_inv_val, ClosedSubmodule.mem_orthogonal, Units.smul_def, ClosedSubmodule.mem_mapEquiv_iff
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
mp : (∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0) → ∀ y ∈ S, ⟪y, x⟫.im = 0
mpr : (∀ y ∈ S, ⟪y, x⟫.im = 0) → ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
⊢ (∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0) ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
y : H
hy : y ∈ S
⊢ -(I • I • y) ∈ S → inner ℝ (I • y) x = 0

Tactic:
have hiy := h (I • y)
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
y : H
hy : y ∈ S
hiy : -(I • I • y) ∈ S → inner ℝ (I • y) x = 0
⊢ y ∈ S → inner ℝ (I • y) x = 0

Tactic:
simp only [← smul_assoc, smul_eq_mul, I_mul_I, neg_smul, one_smul, neg_neg] at hiy

Premises used: neg_smul, smul_assoc, neg_neg, one_smul, Complex.I_mul_I, smul_eq_mul
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
y : H
hy : y ∈ S
hiy : y ∈ S → inner ℝ (I • y) x = 0
⊢ ⟪y, x⟫.im = 0

Tactic:
simpa [inner_real_eq_re_inner] using hiy hy

Premises used: ClosedSubmodule.inner_real_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ y ∈ S, ⟪y, x⟫.im = 0
mpr : ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
⊢ ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0

Tactic:
_
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ y ∈ S, ⟪y, x⟫.im = 0
u : H
hy : -(I • u) ∈ S
⊢ ⟪-(I • u), x⟫.im = 0

Tactic:
have hiy := h _ hy
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ y ∈ S, ⟪y, x⟫.im = 0
u : H
hy : -(I • u) ∈ S
hiy : ⟪-(I • u), x⟫.im = 0
⊢ inner ℝ u x = 0

Tactic:
simpa [inner_smul_left] using hiy

Premises used: inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
carrier : ∀ (x : H), x ∈ (↑Sᗮ.mulI : Submodule ℝ H).carrier ↔ x ∈ (↑S.symplComp : Submodule ℝ H).carrier
⊢ Sᗮ.mulI = S.symplComp

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
carrier : UnitI.inv • x ∈ Sᗮ ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0
⊢ x ∈ (↑Sᗮ.mulI : Submodule ℝ H).carrier ↔ x ∈ (↑S.symplComp : Submodule ℝ H).carrier

Tactic:
rw [← mem_iff, ← mem_iff, mem_symplComp_iff, mem_mapEquiv_iff, scalarSMulCLE_symm_apply,
    Units.inv_mk, Units.smul_mk_apply]

Premises used: ClosedSubmodule.mem_iff, scalarSMulCLE_symm_apply, Units.inv_mk, Units.smul_mk_apply, ClosedSubmodule.mem_symplComp_iff, ClosedSubmodule.mem_mapEquiv_iff
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ UnitI.inv • x ∈ Sᗮ ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0

Tactic:
simp [inner_real_eq_re_inner]

Premises used: ClosedSubmodule.inner_real_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
rw rw₁ : S.symplComp = S.mulIᗮ
⊢ Sᗮ.mulI = S.mulIᗮ

Tactic:
rw [mulI_orthogonal_eq_symplComp]

Premises used: ClosedSubmodule.mulI_orthogonal_eq_symplComp
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
rw : mulI S.mulIᗮ = S.mulI.symplComp
rw₁ : Eq.{u_1 + 1} (α := ClosedSubmodule ℝ H) (mulI S.mulIᗮ) S.mulI.mulIᗮ
rw₂ rw₃ : S.mulI.symplComp = S.mulI.mulIᗮ
⊢ S.symplComp.mulI = S.mulI.symplComp

Tactic:
rw [symplComp, symplComp, mulI_orthogonal_eq_symplComp]

Premises used: ClosedSubmodule.symplComp, ClosedSubmodule.mulI_orthogonal_eq_symplComp
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
carrier : ∀ (x : H), x ∈ (↑S.mulI.mulI : Submodule ℝ H).carrier ↔ x ∈ (↑S : Submodule ℝ H).carrier
⊢ S.mulI.mulI = S

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
carrier : x ∈ S.mulI.mulI → x ∈ S
carrier₁ : x ∈ S → x ∈ S.mulI.mulI
⊢ x ∈ S.mulI.mulI ↔ x ∈ S

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
h : x ∈ S.mulI.mulI
⊢ ∀ (a : ℝ), HSMul.hSMul (β := H) a ((ContinuousLinearEquiv.symm (scalarSMulCLE H UnitI) : (a : H) → H) x : H) ∈ S.mulI

Tactic:
rw [mem_mapEquiv_iff (scalarSMulCLE H UnitI), ← SetLike.forall_smul_mem_iff] at h

Premises used: scalarSMulCLE, SetLike.forall_smul_mem_iff, Complex.UnitI, ClosedSubmodule.mem_mapEquiv_iff