awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (goal)
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 : ℕ
E' : Type u_3
inst_4 : NormedAddCommGroup E'
inst_5 : InnerProductSpace 𝕜 E'
inst_6 : FiniteDimensional 𝕜 E'
T' : E' →ₗ[𝕜] E'
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
hT' : IsSymmetric.{u_1, u_3} (𝕜 := 𝕜) (E := E') T'
hn' : finrank 𝕜 E' = n
h : T.charpoly = T'.charpoly
rw : List.ofFn (hT.eigenvalues hn) = List.ofFn (hT'.eigenvalues hn')
rw₁ :
  (Multiset.sort (Multiset.map (⇑RCLike.re : (a : 𝕜) → ℝ) T.charpoly.roots) fun (x1 x2 : ℝ) ↦ x1 ≥ x2) =
    List.ofFn (hT'.eigenvalues hn')
rw₂ :
  Eq (α := List ℝ) (Multiset.sort (Multiset.map (⇑RCLike.re : (a : 𝕜) → ℝ) T.charpoly.roots) fun (x1 x2 : ℝ) ↦ x1 ≥ x2)
    (Multiset.sort (Multiset.map (⇑RCLike.re : (a : 𝕜) → ℝ) T'.charpoly.roots) fun (x1 x2 : ℝ) ↦ x1 ≥ x2)
⊢ hT.eigenvalues hn = hT'.eigenvalues hn'
have rw₃ : Eq (α := List ℝ) (Multiset.sort (Multiset.map (⇑RCLike.re : (a : 𝕜) → ℝ) T'.charpoly.roots) fun (x1 x2 : ℝ) ↦ x1 ≥ x2)
  (Multiset.sort (Multiset.map (⇑RCLike.re : (a : 𝕜) → ℝ) T'.charpoly.roots) fun (x1 x2 : ℝ) ↦ x1 ≥ x2)
Tactic: rw [← List.ofFn_inj, ← sort_roots_charpoly_eq_eigenvalues, ← sort_roots_charpoly_eq_eigenvalues,
      h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (goal)
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
⊢ T.charpoly.Splits
have refine : T.charpoly.roots.card = T.charpoly.natDegree
Tactic: refine Polynomial.splits_iff_card_roots.mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T (↑μ : 𝕜)
hnn : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫ : ℝ)
⊢ 0 ≤ μ
have obtain : ∀ (v : E)
  (hv₁ :
    Membership.mem (γ := Submodule 𝕜 E) ((genEigenspace T (↑μ : 𝕜) : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) v)
  (hv₂ : v ≠ 0), 0 ≤ μ
Tactic: obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T (↑μ : 𝕜)
hnn : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫ : ℝ)
v : E
hv₁ : Membership.mem (γ := Submodule 𝕜 E) ((genEigenspace T (↑μ : 𝕜) : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) v
hv₂ : v ≠ 0
⊢ 0 ≤ μ
have hpos : 0 < HPow.hPow (β := ℕ) ‖v‖ 2
Tactic: have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv₂
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T (↑μ : 𝕜)
hnn : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫ : ℝ)
v : E
hv₁ : Membership.mem (γ := Submodule 𝕜 E) ((genEigenspace T (↑μ : 𝕜) : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) v
hv₂ : v ≠ 0
hpos : 0 < HPow.hPow (β := ℕ) ‖v‖ 2
⊢ 0 ≤ μ
have hv₃ : (T : (a : E) → E) v = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑μ : 𝕜) v
Tactic: simp only [mem_genEigenspace_one] at hv₁
Cleared hypotheses: hv₁
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T (↑μ : 𝕜)
hnn : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫ : ℝ)
v : E
hv₂ : v ≠ 0
hpos : 0 < HPow.hPow (β := ℕ) ‖v‖ 2
hv₁ : (T : (a : E) → E) v = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑μ : 𝕜) v
⊢ 0 ≤ μ
have this : (RCLike.re : (a : 𝕜) → ℝ) ⟪v, (T : (a : E) → E) v⟫ = μ * HPow.hPow (β := ℕ) ‖v‖ 2
Tactic: have : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 :=
    mod_cast congr_arg RCLike.re (inner_product_apply_eigenvector hv₁)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T (↑μ : 𝕜)
hnn : ∀ (x : E), LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫ : ℝ)
⊢ 0 < μ
have obtain : ∀ (v : E)
  (hv₁ :
    Membership.mem (γ := Submodule 𝕜 E) ((genEigenspace T (↑μ : 𝕜) : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) v)
  (hv₂ : v ≠ 0), 0 < μ
Tactic: obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T (↑μ : 𝕜)
hnn : ∀ (x : E), LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫ : ℝ)
v : E
hv₁ : Membership.mem (γ := Submodule 𝕜 E) ((genEigenspace T (↑μ : 𝕜) : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) v
hv₂ : v ≠ 0
⊢ 0 < μ
have hpos : 0 < HPow.hPow (β := ℕ) ‖v‖ 2
Tactic: have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv₂
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T (↑μ : 𝕜)
hnn : ∀ (x : E), LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫ : ℝ)
v : E
hv₁ : Membership.mem (γ := Submodule 𝕜 E) ((genEigenspace T (↑μ : 𝕜) : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) v
hv₂ : v ≠ 0
hpos : 0 < HPow.hPow (β := ℕ) ‖v‖ 2
⊢ 0 < μ
have hv₃ : (T : (a : E) → E) v = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑μ : 𝕜) v
Tactic: simp only [mem_genEigenspace_one] at hv₁
Cleared hypotheses: hv₁
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T (↑μ : 𝕜)
hnn : ∀ (x : E), LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫ : ℝ)
v : E
hv₂ : v ≠ 0
hpos : 0 < HPow.hPow (β := ℕ) ‖v‖ 2
hv₁ : (T : (a : E) → E) v = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑μ : 𝕜) v
⊢ 0 < μ
have this : (RCLike.re : (a : 𝕜) → ℝ) ⟪v, (T : (a : E) → E) v⟫ = μ * HPow.hPow (β := ℕ) ‖v‖ 2
Tactic: have : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 :=
    mod_cast congr_arg RCLike.re (inner_product_apply_eigenvector hv₁)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (goal)
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)
⊢ (∀ (μ : 𝕜), HasEigenvalue (↑T : E →ₗ[𝕜] E) μ → μ = 0) ↔ T = 0
have rw : (¬∀ (μ : 𝕜), HasEigenvalue (↑T : E →ₗ[𝕜] E) μ → μ = 0) ↔
  ¬∀ (i : 𝕜), Eq (α := ENNReal) (⨆ (_ : i ∈ spectrum 𝕜 T), (↑‖i‖₊ : ENNReal)) 0
Tactic: rw [← nnnorm_eq_zero, ← ENNReal.coe_eq_zero, ← T.spectralRadius_eq_nnnorm hT'.isSelfAdjoint,
    spectralRadius, ← not_iff_not, ENNReal.iSup_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (goal)
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)
⊢ (¬∀ (μ : 𝕜), HasEigenvalue (↑T : E →ₗ[𝕜] E) μ → μ = 0) ↔
    ¬∀ (i : 𝕜), Eq (α := ENNReal) (⨆ (_ : i ∈ spectrum 𝕜 T), (↑‖i‖₊ : ENNReal)) 0
have push : (∃ (μ : 𝕜), HasEigenvalue (↑T : E →ₗ[𝕜] E) μ ∧ μ ≠ 0) ↔
  ∃ (i : 𝕜), Ne (α := ENNReal) (⨆ (_ : i ∈ spectrum 𝕜 T), (↑‖i‖₊ : ENNReal)) 0
Tactic: push Not
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (goal)
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)
⊢ (∃ (μ : 𝕜), HasEigenvalue (↑T : E →ₗ[𝕜] E) μ ∧ μ ≠ 0) ↔
    ∃ (i : 𝕜), Ne (α := ENNReal) (⨆ (_ : i ∈ spectrum 𝕜 T), (↑‖i‖₊ : ENNReal)) 0
have h : ∀ (a : 𝕜), HasEigenvalue (↑T : E →ₗ[𝕜] E) a ∧ a ≠ 0 ↔ Ne (α := ENNReal) (⨆ (_ : a ∈ spectrum 𝕜 T), (↑‖a‖₊ : ENNReal)) 0
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
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 ⋯
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ ⊥
have hS_compact : 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
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) μ)ᗮ)
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ ⊥
have hS_symm : 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)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
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) μ)ᗮ)
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ ⊥
have hS : ∀ (μ : 𝕜),
  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 _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
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) μ)ᗮ)
        μ =
      ⊥
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ ⊥
have h : ∀ (μ : 𝕜),
  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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ ⊥
have h₁ : S = 0
Tactic: rw [eq_zero_of_forall_hasEigenvalue_eq_zero hS_compact hS_symm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (goal)
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
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ ⊥
have rw : Subsingleton.{u_2 + 1} ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ
Tactic: rw [← Submodule.subsingleton_iff_eq_bot]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (goal)
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
⊢ Subsingleton.{u_2 + 1} ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ
have by_contra! : ∀ (hV : Nontrivial.{u_2} ↥(⨆ (μ : 𝕜), eigenspace (↑T : E →ₗ[𝕜] E) μ)ᗮ), False
Tactic: by_contra! hV
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
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
⊢ FiniteDimensional.{u_1, u_2} 𝕜 ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)
have hT₁ : IsCompactOperator (M₁ := ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)) (M₂ := ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ))
  (⇑((↑T : E →ₗ[𝕜] E).restrict sorry) : (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 μ))
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (hypothesis)
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) μ))
⊢ FiniteDimensional.{u_1, u_2} 𝕜 ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)
have 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) μ))
Tactic: rw [restrict_eigenspace, LinearMap.coe_smul, IsCompactOperator.smul_iff₀ hμ] at hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Spectrum (goal)
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) μ))
⊢ FiniteDimensional.{u_1, u_2} 𝕜 ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)
have rwa : IsCompactOperator.{u_2, u_2} (M₁ := ↥(eigenspace (↑T : E →ₗ[𝕜] E) μ)) id
Tactic: rwa [← isCompactOperator_id_iff_finiteDimensional]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x y : H
⊢ (starRingEnd ℝ : (a : ℝ) → ℝ) ⟪y, x⟫.re = ⟪x, y⟫.re
have simp : ⟪y, x⟫.re = re ((starRingEnd ℂ : (a : ℂ) → ℂ) ⟪y, x⟫)
Tactic: simp only [← ipc.conj_inner_symm x y, conj_trivial]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
⊢ x ∈ S.symplComp ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0
have simp : (∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0) ↔ ∀ 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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
⊢ (∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0) ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0
have mp : (∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0) → ∀ y ∈ S, ⟪y, x⟫.im = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
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
⊢ (∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0) ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0
have mpr : (∀ y ∈ S, ⟪y, x⟫.im = 0) → ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (hypothesis)
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
⊢ ⟪y, x⟫.im = 0
have hiy : -(I • I • y) ∈ S → inner ℝ (I • y) x = 0
Tactic: have hiy := h (I • y)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (hypothesis)
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, x⟫.im = 0
have hiy₁ : 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
Cleared hypotheses: hiy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (hypothesis)
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
⊢ inner ℝ u x = 0
have hiy : ⟪-(I • u), x⟫.im = 0
Tactic: have hiy := h _ hy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
⊢ Sᗮ.mulI = S.symplComp
have carrier : ∀ (x : H), x ∈ (↑Sᗮ.mulI : Submodule ℝ H).carrier ↔ x ∈ (↑S.symplComp : Submodule ℝ H).carrier
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ (↑Sᗮ.mulI : Submodule ℝ H).carrier ↔ x ∈ (↑S.symplComp : Submodule ℝ H).carrier
have carrier : UnitI.inv • x ∈ Sᗮ ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0
Tactic: rw [← mem_iff, ← mem_iff, mem_symplComp_iff, mem_mapEquiv_iff, scalarSMulCLE_symm_apply,
    Units.inv_mk, Units.smul_mk_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
⊢ Sᗮ.mulI = S.mulIᗮ
have rw : S.symplComp = S.mulIᗮ
Tactic: rw [mulI_orthogonal_eq_symplComp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StandardSubspace (goal)
Goal:
H : Type u_1
inst : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
⊢ S.symplComp.mulI = S.mulI.symplComp
have rw : mulI S.mulIᗮ = S.mulI.symplComp
Tactic: rw [symplComp, symplComp, mulI_orthogonal_eq_symplComp]