awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
⊢ T.singularValues.support = Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range)
have obtain : ∀ (n : ℕ) (hn : (↑T.singularValues.support : Set ℕ) = Set.Iio n),
  T.singularValues.support = Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range)
Tactic: obtain ⟨n, hn⟩ := T.isLowerSet_support_singularValues.eq_univ_or_Iio.resolve_left
    (fun h ↦ Set.infinite_univ.not_finite (h ▸ Finset.finite_toSet _))
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
hn : (↑T.singularValues.support : Set ℕ) = Set.Iio n
⊢ T.singularValues.support = Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range)
have hn₁ : T.singularValues.support = Finset.range n
Tactic: rw [← Finset.coe_Iio, Finset.coe_inj, Nat.Iio_eq_range] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
⊢ LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
have rw : Ne (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
Tactic: rw [singularValues_pos_iff_ne_zero, ← Finsupp.mem_support_iff, support_singularValues,
    Finset.mem_range]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
rw : Ne (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
⊢ LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
have rw₁ : n ∈ T.singularValues.support ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
Tactic: rw [singularValues_pos_iff_ne_zero, ← Finsupp.mem_support_iff, support_singularValues,
    Finset.mem_range]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
rw : Ne (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
rw₁ : n ∈ T.singularValues.support ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
⊢ LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
have rw₂ : n ∈ Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range) ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
Tactic: rw [singularValues_pos_iff_ne_zero, ← Finsupp.mem_support_iff, support_singularValues,
    Finset.mem_range]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
rw : Ne (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
rw₁ : n ∈ T.singularValues.support ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
rw₂ : n ∈ Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range) ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
⊢ LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
have rw₃ : n < finrank.{u_1, u_3} 𝕜 ↥T.range ↔ n < finrank.{u_1, u_3} 𝕜 ↥T.range
Tactic: rw [singularValues_pos_iff_ne_zero, ← Finsupp.mem_support_iff, support_singularValues,
    Finset.mem_range]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
⊢ Eq (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) (finrank.{u_1, u_3} 𝕜 ↥T.range) : ℝ) (0 : ℝ)
have rw : finrank.{u_1, u_3} 𝕜 ↥T.range ∉ Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range)
Tactic: rw [← Finsupp.notMem_support_iff, support_singularValues]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
⊢ Eq (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
have rw : n ∉ T.singularValues.support ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
Tactic: rw [← Finsupp.notMem_support_iff, support_singularValues, Finset.mem_range, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
rw : n ∉ T.singularValues.support ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
⊢ Eq (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
have rw₁ : n ∉ Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range) ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
Tactic: rw [← Finsupp.notMem_support_iff, support_singularValues, Finset.mem_range, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
rw : n ∉ T.singularValues.support ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
rw₁ : n ∉ Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range) ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
⊢ Eq (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
have rw₂ : ¬n < finrank.{u_1, u_3} 𝕜 ↥T.range ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
Tactic: rw [← Finsupp.notMem_support_iff, support_singularValues, Finset.mem_range, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
rw : n ∉ T.singularValues.support ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
rw₁ : n ∉ Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range) ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
rw₂ : ¬n < finrank.{u_1, u_3} 𝕜 ↥T.range ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
⊢ Eq (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
have rw₃ : finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
Tactic: rw [← Finsupp.notMem_support_iff, support_singularValues, Finset.mem_range, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
⊢ singularValues.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) (F := F) 0 = 0
have h : ∀ (i : ℕ),
  Eq (α := ℝ) ((singularValues.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) (F := F) 0 : (a : ℕ) → ℝ) i : ℝ)
    ((0 : (a : ℕ) → ℝ) i : ℝ)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
i : ℕ
⊢ Eq (α := ℝ) ((singularValues.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) (F := F) 0 : (a : ℕ) → ℝ) i : ℝ)
    ((0 : (a : ℕ) → ℝ) i : ℝ)
have h : finrank.{u_1, u_3} 𝕜 ↥⊥ ≤ i
Tactic: rw [Finsupp.zero_apply, singularValues_eq_zero_iff_le_finrank_range, range_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
⊢ T.singularValues = 0 ↔ T = 0
have mp : T.singularValues = 0 → T = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
mp : T.singularValues = 0 → T = 0
⊢ T.singularValues = 0 ↔ T = 0
have mpr : T = 0 → T.singularValues = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
h : T.singularValues = 0
⊢ T = 0
have mp : T.range = ⊥
Tactic: rw [← range_eq_bot, ← Submodule.finrank_eq_zero, ← Nat.le_zero,
      ← singularValues_eq_zero_iff_le_finrank_range, h, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
h : T.singularValues = 0
mp : T.range = ⊥
⊢ T = 0
have mp₁ : finrank.{u_1, u_3} 𝕜 ↥T.range = 0
Tactic: rw [← range_eq_bot, ← Submodule.finrank_eq_zero, ← Nat.le_zero,
      ← singularValues_eq_zero_iff_le_finrank_range, h, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
h : T.singularValues = 0
mp : T.range = ⊥
mp₁ : finrank.{u_1, u_3} 𝕜 ↥T.range = 0
⊢ T = 0
have mp₂ : finrank.{u_1, u_3} 𝕜 ↥T.range ≤ 0
Tactic: rw [← range_eq_bot, ← Submodule.finrank_eq_zero, ← Nat.le_zero,
      ← singularValues_eq_zero_iff_le_finrank_range, h, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
h : T.singularValues = 0
mp : T.range = ⊥
mp₁ : finrank.{u_1, u_3} 𝕜 ↥T.range = 0
mp₂ : finrank.{u_1, u_3} 𝕜 ↥T.range ≤ 0
⊢ T = 0
have mp₃ : Eq (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) 0 : ℝ) (0 : ℝ)
Tactic: rw [← range_eq_bot, ← Submodule.finrank_eq_zero, ← Nat.le_zero,
      ← singularValues_eq_zero_iff_le_finrank_range, h, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
h : T.singularValues = 0
mp : T.range = ⊥
mp₁ : finrank.{u_1, u_3} 𝕜 ↥T.range = 0
mp₂ : finrank.{u_1, u_3} 𝕜 ↥T.range ≤ 0
mp₃ : Eq (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) 0 : ℝ) (0 : ℝ)
⊢ T = 0
have mp₄ : Eq (α := ℝ) ((0 : (a : ℕ) → ℝ) 0 : ℝ) (0 : ℝ)
Tactic: rw [← range_eq_bot, ← Submodule.finrank_eq_zero, ← Nat.le_zero,
      ← singularValues_eq_zero_iff_le_finrank_range, h, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
h : T.singularValues = 0
mp : T.range = ⊥
mp₁ : finrank.{u_1, u_3} 𝕜 ↥T.range = 0
mp₂ : finrank.{u_1, u_3} 𝕜 ↥T.range ≤ 0
mp₃ : Eq (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) 0 : ℝ) (0 : ℝ)
mp₄ : Eq (α := ℝ) ((0 : (a : ℕ) → ℝ) 0 : ℝ) (0 : ℝ)
⊢ T = 0
have mp₅ : Eq (α := ℝ) 0 0
Tactic: rw [← range_eq_bot, ← Submodule.finrank_eq_zero, ← Nat.le_zero,
      ← singularValues_eq_zero_iff_le_finrank_range, h, Finsupp.zero_apply]
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
⊢ (T : (a : E) → E) w = μ • w
have rwa : ∀ (hw : (T : (a : E) → E) w = μ • w), (T : (a : E) → E) w = μ • w
Tactic: rwa [mem_eigenspace_iff] at hw
Cleared hypotheses: hw
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
⊢ ⟪w, (T : (a : E) → E) v⟫ = 0
have this : (T : (a : E) → E) w = μ • w
Tactic: have : T w = (μ : 𝕜) • w := by rwa [mem_eigenspace_iff] at hw
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
hμ : HasEigenvalue T μ
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ
have obtain : ∀ (v : E)
  (hv₁ : Membership.mem (γ := Submodule 𝕜 E) ((genEigenspace T μ : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) v)
  (hv₂ : v ≠ 0), (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ
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
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
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ
have hv₃ : (T : (a : E) → E) v = μ • v
Tactic: rw [mem_eigenspace_iff] at hv₁
Cleared hypotheses: hv₁, 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
⊢ 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
have 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
Tactic: by_cases hv' : v = 0
-- 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
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
⊢ 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
have 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
Tactic: by_cases hv' : v = 0
-- 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
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
have H : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) μ = μ
Tactic: have H := hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector ⟨hv, 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
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 : 𝕜) → 𝕜) μ = μ
⊢ 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
have 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
Tactic: rw [mem_eigenspace_iff] at hv hw
Cleared hypotheses: w, hw, hv', 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
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
have 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
Tactic: refine Or.resolve_left ?_ hμν.symm
-- 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
v : E
hv : Membership.mem (γ := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ v
⊢ Membership.mem (α := E) (γ := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ ((T : (a : E) → E) v : E)
have 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)
Tactic: rw [← Submodule.iInf_orthogonal] at hv ⊢
Cleared hypotheses: 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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ eigenspace (T.restrict ⋯) μ = ⊥
have refine : Disjoint (eigenspace T μ) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
Tactic: refine eigenspace_restrict_eq_bot 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
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ Disjoint (eigenspace T μ) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
have H₂ : eigenspace T μ ⟂ p
Tactic: have H₂ : eigenspace T μ ⟂ p := (Submodule.isOrtho_orthogonal_right _).mono_left (le_iSup _ _)