awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
i j : Fin n
a :
  Eq.{u_1 + 1} (α := 𝕜) (if i = j then (↑(hT.eigenvalues hn j) : 𝕜) else 0)
    (if i = j then (↑(hT.eigenvalues hn i) : 𝕜) else 0)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((toMatrix (hT.eigenvectorBasis hn).toBasis (hT.eigenvectorBasis hn).toBasis :
          (a : E →ₗ[𝕜] E) → Matrix (Fin n) (Fin n) 𝕜)
        T i j :
      𝕜)
    (Matrix.diagonal (RCLike.ofReal ∘ hT.eigenvalues hn) i j : 𝕜)

Tactic:
simp [toMatrix_apply, Matrix.diagonal_apply, RCLike.real_smul_eq_coe_mul]

Premises used: Matrix.diagonal_apply, RCLike.real_smul_eq_coe_mul, LinearMap.toMatrix_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
i j : Fin n
⊢ Eq.{u_1 + 1} (α := 𝕜) (if i = j then (↑(hT.eigenvalues hn j) : 𝕜) else 0)
    (if i = j then (↑(hT.eigenvalues hn i) : 𝕜) else 0)

Tactic:
grind
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
⊢ T.charpoly = ∏ i : Fin n, HSub.hSub (α := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) (↑(hT.eigenvalues hn i) : 𝕜))

Tactic:
simp [← T.charpoly_toMatrix (hT.eigenvectorBasis hn).toBasis, toMatrix_eigenvectorBasis,
    Matrix.charpoly_diagonal]

Premises used: LinearMap.IsSymmetric.eigenvectorBasis, LinearMap.IsSymmetric.toMatrix_eigenvectorBasis, Matrix.charpoly_diagonal, OrthonormalBasis.toBasis, LinearMap.charpoly_toMatrix
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
⊢ Ne.{u_1 + 1} (α := Polynomial 𝕜)
    (∏ i : Fin n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X
        ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) ((RCLike.ofReal ∘ hT.eigenvalues hn) i)))
    0

Tactic:
simp [Finset.prod_ne_zero_iff, Polynomial.X_sub_C_ne_zero]

Premises used: Finset.prod_ne_zero_iff, Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
rw :
  Eq.{u_1 + 1} (α := Multiset 𝕜)
    (Multiset.bind (Finset.val Finset.univ) fun (i : Fin n) ↦
      (HSub.hSub (α := Polynomial 𝕜) Polynomial.X
          ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) ((RCLike.ofReal ∘ hT.eigenvalues hn) i))).roots)
    (Multiset.map (RCLike.ofReal ∘ hT.eigenvalues hn) (Finset.val Finset.univ))
⊢ T.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hT.eigenvalues hn) (Finset.val Finset.univ)

Tactic:
rw [← charpoly_toMatrix _ (hT.eigenvectorBasis hn).toBasis, toMatrix_eigenvectorBasis,
    Matrix.charpoly_diagonal, Polynomial.roots_prod _ _ (by
      simp [Finset.prod_ne_zero_iff, Polynomial.X_sub_C_ne_zero])]

Premises used: LinearMap.IsSymmetric.eigenvectorBasis, Polynomial.roots_prod, LinearMap.IsSymmetric.toMatrix_eigenvectorBasis, Matrix.charpoly_diagonal, OrthonormalBasis.toBasis, LinearMap.charpoly_toMatrix
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
⊢ Eq.{u_1 + 1} (α := Multiset 𝕜)
    (Multiset.bind (Finset.val Finset.univ) fun (i : Fin n) ↦
      (HSub.hSub (α := Polynomial 𝕜) Polynomial.X
          ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) ((RCLike.ofReal ∘ hT.eigenvalues hn) i))).roots)
    (Multiset.map (RCLike.ofReal ∘ hT.eigenvalues hn) (Finset.val Finset.univ))

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
simp_rw :
  (List.mergeSort (List.ofFn (n := finrank 𝕜 E) fun (x : Fin (finrank 𝕜 E)) ↦ hT.eigenvalues ⋯ x) fun (x1 x2 : ℝ) ↦
      decide (x1 ≥ x2)) =
    List.ofFn (hT.eigenvalues hn)
⊢ (Multiset.sort (Multiset.map (⇑RCLike.re : (a : 𝕜) → ℝ) T.charpoly.roots) fun (x1 x2 : ℝ) ↦ x1 ≥ x2) =
    List.ofFn (hT.eigenvalues hn)

Tactic:
simp_rw [hT.roots_charpoly_eq_eigenvalues, Fin.univ_val_map, Multiset.map_coe, List.map_ofFn,
    Function.comp_def, RCLike.ofReal_re, Multiset.coe_sort]

Premises used: RCLike.ofReal_re, List.map_ofFn, Function.comp_def, Multiset.coe_sort, LinearMap.IsSymmetric.roots_charpoly_eq_eigenvalues, Multiset.map_coe, Fin.univ_val_map
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
⊢ n = finrank 𝕜 E

Tactic:
have := hn.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
this : n = finrank 𝕜 E
⊢ Eq (α := List ℝ)
    (List.mergeSort (List.ofFn (n := finrank 𝕜 E) fun (x : Fin (finrank 𝕜 E)) ↦ hT.eigenvalues ⋯ x) fun (x1 x2 : ℝ) ↦
      decide (x1 ≥ x2))
    (List.ofFn (n := finrank 𝕜 E) fun (x : Fin (finrank 𝕜 E)) ↦ hT.eigenvalues ⋯ x)

Tactic:
List.mergeSort_of_pairwise ?_

Premises used: List.mergeSort_of_pairwise
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
this : n = finrank 𝕜 E
convert_4 :
  List.Pairwise (fun (a b : ℝ) ↦ decide (a ≥ b) = true)
    (List.ofFn (n := finrank 𝕜 E) fun (x : Fin (finrank 𝕜 E)) ↦ hT.eigenvalues ⋯ x)
⊢ (List.mergeSort (List.ofFn (n := finrank 𝕜 E) fun (x : Fin (finrank 𝕜 E)) ↦ hT.eigenvalues ⋯ x) fun (x1 x2 : ℝ) ↦
      decide (x1 ≥ x2)) =
    List.ofFn (hT.eigenvalues hn)

Tactic:
convert! List.mergeSort_of_pairwise ?_

Premises used: List.mergeSort_of_pairwise
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
this : n = finrank 𝕜 E
convert_4 : List.SortedGE (α := ℝ) (List.ofFn (n := finrank 𝕜 E) fun (x : Fin (finrank 𝕜 E)) ↦ hT.eigenvalues ⋯ x)
⊢ List.Pairwise (fun (a b : ℝ) ↦ decide (a ≥ b) = true)
    (List.ofFn (n := finrank 𝕜 E) fun (x : Fin (finrank 𝕜 E)) ↦ hT.eigenvalues ⋯ x)

Tactic:
simp_rw [decide_eq_true_eq, ← List.sortedGE_iff_pairwise]

Premises used: List.sortedGE_iff_pairwise, decide_eq_true_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
this : n = finrank 𝕜 E
⊢ (List.ofFn (hT.eigenvalues hn)).SortedGE

Tactic:
(hT.eigenvalues_antitone hn).sortedGE_ofFn

Premises used: Antitone.sortedGE_ofFn, LinearMap.IsSymmetric.eigenvalues_antitone
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
this : n = finrank 𝕜 E
⊢ List.SortedGE (α := ℝ) (List.ofFn (n := finrank 𝕜 E) fun (x : Fin (finrank 𝕜 E)) ↦ hT.eigenvalues ⋯ x)

Tactic:
convert! (hT.eigenvalues_antitone hn).sortedGE_ofFn

Premises used: Antitone.sortedGE_ofFn, LinearMap.IsSymmetric.eigenvalues_antitone
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
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 : hT.eigenvalues hn = hT'.eigenvalues hn'
rw :
  ∏ i : Fin n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X
        ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hT.eigenvalues hn i) : 𝕜)) =
    T'.charpoly
rw₁ :
  Eq.{u_1 + 1} (α := Polynomial 𝕜)
    (∏ i : Fin n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hT.eigenvalues hn i) : 𝕜)))
    (∏ i : Fin n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X
        ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hT'.eigenvalues hn' i) : 𝕜)))
rw₂ rw₃ :
  Eq.{u_1 + 1} (α := Polynomial 𝕜)
    (∏ i : Fin n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X
        ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hT'.eigenvalues hn' i) : 𝕜)))
    (∏ i : Fin n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X
        ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hT'.eigenvalues hn' i) : 𝕜)))
⊢ T.charpoly = T'.charpoly

Tactic:
rw [hT.charpoly_eq hn, hT'.charpoly_eq hn', h]

Premises used: LinearMap.IsSymmetric.charpoly_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
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)
rw₃ 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'

Tactic:
rw [← List.ofFn_inj, ← sort_roots_charpoly_eq_eigenvalues, ← sort_roots_charpoly_eq_eigenvalues,
      h]

Premises used: List.ofFn_inj, LinearMap.IsSymmetric.sort_roots_charpoly_eq_eigenvalues
-- 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
⊢ T.charpoly.Splits

Tactic:
Polynomial.splits_iff_card_roots.mpr ?_

Premises used: Iff.mpr, Polynomial.splits_iff_card_roots
-- 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
refine : T.charpoly.roots.card = T.charpoly.natDegree
⊢ T.charpoly.Splits

Tactic:
refine Polynomial.splits_iff_card_roots.mpr ?_

Premises used: Iff.mpr, Polynomial.splits_iff_card_roots
-- 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
⊢ T.charpoly.roots.card = T.charpoly.natDegree

Tactic:
simp [hT.roots_charpoly_eq_eigenvalues rfl, LinearMap.charpoly_natDegree]

Premises used: LinearMap.charpoly_natDegree, LinearMap.IsSymmetric.roots_charpoly_eq_eigenvalues, 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
n : ℕ
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
hn : finrank 𝕜 E = n
⊢ Eq.{u_1 + 1} (α := 𝕜) ((LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) T : 𝕜) (∏ i : Fin n, (↑(hT.eigenvalues hn i) : 𝕜) : 𝕜)

Tactic:
simp [det_eq_prod_roots_charpoly_of_splits hT.splits_charpoly,
    hT.roots_charpoly_eq_eigenvalues hn, List.prod_ofFn]

Premises used: LinearMap.IsSymmetric.splits_charpoly, Module.End.det_eq_prod_roots_charpoly_of_splits, List.prod_ofFn, LinearMap.IsSymmetric.roots_charpoly_eq_eigenvalues
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
μ : 𝕜
v : E
T : E →ₗ[𝕜] E
h : (T : (a : E) → E) v = μ • v
⊢ ⟪v, (T : (a : E) → E) v⟫ = μ * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2

Tactic:
simp only [h, inner_smul_right, inner_self_eq_norm_sq_to_K]

Premises used: inner_self_eq_norm_sq_to_K, inner_smul_right
-- 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
hμ : HasEigenvalue T (↑μ : 𝕜)
hnn : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫ : ℝ)
obtain :
  ∀ (v : E)
    (hv₁ :
      Membership.mem (γ := Submodule 𝕜 E) ((genEigenspace T (↑μ : 𝕜) : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) v)
    (hv₂ : v ≠ 0), 0 ≤ μ
⊢ 0 ≤ μ

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
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 < HPow.hPow (β := ℕ) ‖v‖ 2

Tactic:
simpa only [sq_pos_iff, norm_ne_zero_iff] using hv₂

Premises used: norm_ne_zero_iff, sq_pos_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
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 < HPow.hPow (β := ℕ) ‖v‖ 2

Tactic:
have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using 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
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
⊢ (T : (a : E) → E) v = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑μ : 𝕜) v

Tactic:
simp only [mem_genEigenspace_one] at hv₁

Premises used: Module.End.mem_genEigenspace_one
-- 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
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
⊢ (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₁)
-- 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
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
this : (RCLike.re : (a : 𝕜) → ℝ) ⟪v, (T : (a : E) → E) v⟫ = μ * HPow.hPow (β := ℕ) ‖v‖ 2
⊢ 0 ≤ μ

Tactic:
(mul_nonneg_iff_of_pos_right hpos).mp (this ▸ hnn v)

Premises used: mul_nonneg_iff_of_pos_right, Eq.rec, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
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
this : (RCLike.re : (a : 𝕜) → ℝ) ⟪v, (T : (a : E) → E) v⟫ = μ * HPow.hPow (β := ℕ) ‖v‖ 2
⊢ 0 ≤ μ

Tactic:
exact (mul_nonneg_iff_of_pos_right hpos).mp (this ▸ hnn v)

Premises used: mul_nonneg_iff_of_pos_right, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T (↑μ : 𝕜)
hnn : ∀ (x : E), LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫ : ℝ)
obtain :
  ∀ (v : E)
    (hv₁ :
      Membership.mem (γ := Submodule 𝕜 E) ((genEigenspace T (↑μ : 𝕜) : (a : ℕ∞) → Submodule 𝕜 E) 1 : Submodule 𝕜 E) v)
    (hv₂ : v ≠ 0), 0 < μ
⊢ 0 < μ

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
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 < HPow.hPow (β := ℕ) ‖v‖ 2

Tactic:
simpa only [sq_pos_iff, norm_ne_zero_iff] using hv₂

Premises used: norm_ne_zero_iff, sq_pos_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
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 < HPow.hPow (β := ℕ) ‖v‖ 2

Tactic:
have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using 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
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
⊢ (T : (a : E) → E) v = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑μ : 𝕜) v

Tactic:
simp only [mem_genEigenspace_one] at hv₁

Premises used: Module.End.mem_genEigenspace_one
-- 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
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
⊢ (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₁)
-- 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
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
this : (RCLike.re : (a : 𝕜) → ℝ) ⟪v, (T : (a : E) → E) v⟫ = μ * HPow.hPow (β := ℕ) ‖v‖ 2
⊢ 0 < μ

Tactic:
(mul_pos_iff_of_pos_right hpos).mp (this ▸ hnn v)

Premises used: Eq.rec, mul_pos_iff_of_pos_right, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
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
this : (RCLike.re : (a : 𝕜) → ℝ) ⟪v, (T : (a : E) → E) v⟫ = μ * HPow.hPow (β := ℕ) ‖v‖ 2
⊢ 0 < μ

Tactic:
exact (mul_pos_iff_of_pos_right hpos).mp (this ▸ hnn v)

Premises used: mul_pos_iff_of_pos_right, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
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)
rw :
  (¬∀ (μ : 𝕜), HasEigenvalue (↑T : E →ₗ[𝕜] E) μ → μ = 0) ↔
    ¬∀ (i : 𝕜), Eq (α := ENNReal) (⨆ (_ : i ∈ spectrum 𝕜 T), (↑‖i‖₊ : ENNReal)) 0
⊢ (∀ (μ : 𝕜), HasEigenvalue (↑T : E →ₗ[𝕜] E) μ → μ = 0) ↔ T = 0

Tactic:
rw [← nnnorm_eq_zero, ← ENNReal.coe_eq_zero, ← T.spectralRadius_eq_nnnorm hT'.isSelfAdjoint,
    spectralRadius, ← not_iff_not, ENNReal.iSup_eq_zero]

Premises used: not_iff_not, LinearMap.IsSymmetric.isSelfAdjoint, ENNReal.coe_eq_zero, spectralRadius, nnnorm_eq_zero, ContinuousLinearMap.spectralRadius_eq_nnnorm, ENNReal.iSup_eq_zero