awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
this :
  ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) = ⊥ ↔
    ¬End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0
h : End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0
i : Fin (finrank 𝕜 E)
hi :
  Eq.{u_1 + 1} (α := 𝕜) (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ i) : 𝕜) 0
right : LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) (↑i : ℕ) : ℝ) (0 : ℝ)
⊢ ∃ i < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)

Tactic:
use i, i.isLt

Premises used: Fin.isLt
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
this :
  ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) = ⊥ ↔
    ¬End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0
h : End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0
i : Fin (finrank 𝕜 E)
hi :
  Eq.{u_1 + 1} (α := 𝕜) (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ i) : 𝕜) 0
⊢ LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) (↑i : ℕ) : ℝ) (0 : ℝ)

Tactic:
simp [RCLike.ofReal_eq_zero.mp hi, T.singularValues_fin rfl]

Premises used: LinearMap.singularValues_fin, RCLike.ofReal_eq_zero, Iff.mp, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
this :
  ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) = ⊥ ↔
    ¬End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0
i : ℕ
h : i < finrank 𝕜 E
hz : LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
⊢ End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)
    (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ (⟨i, h⟩ : Fin (finrank 𝕜 E))) :
      𝕜)

Tactic:
T.isSymmetric_adjoint_comp_self.hasEigenvalue_eigenvalues rfl ⟨i, h⟩

Premises used: Fin.mk, LinearMap.IsSymmetric.hasEigenvalue_eigenvalues, LinearMap.isSymmetric_adjoint_comp_self, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
this :
  ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) = ⊥ ↔
    ¬End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0
i : ℕ
h : i < finrank 𝕜 E
hz : LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
h₁ :
  Eq.{u_1 + 1} (α := 𝕜) 0
    (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ (⟨i, h⟩ : Fin (finrank 𝕜 E))) :
      𝕜)
⊢ End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0

Tactic:
convert! T.isSymmetric_adjoint_comp_self.hasEigenvalue_eigenvalues rfl ⟨i, h⟩

Premises used: Fin.mk, LinearMap.IsSymmetric.hasEigenvalue_eigenvalues, LinearMap.isSymmetric_adjoint_comp_self, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
this :
  ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) = ⊥ ↔
    ¬End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0
i : ℕ
h : i < finrank 𝕜 E
hz : LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
h₁ : Eq.{u_1 + 1} (α := 𝕜) 0 (↑(HPow.hPow (α := ℝ) (β := ℕ) 0 2) : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) 0
    (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ (⟨i, h⟩ : Fin (finrank 𝕜 E))) :
      𝕜)

Tactic:
rw [← sq_singularValues_of_lt, le_antisymm hz (T.singularValues_nonneg i)]

Premises used: LinearMap.singularValues_nonneg, LinearMap.sq_singularValues_of_lt, le_antisymm
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
this :
  ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) = ⊥ ↔
    ¬End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0
i : ℕ
h : i < finrank 𝕜 E
hz : LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
⊢ Eq.{u_1 + 1} (α := 𝕜) 0 (↑(HPow.hPow (α := ℝ) (β := ℕ) 0 2) : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
⊢ ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E

Tactic:
grind [singularValues_of_finrank_le]

Premises used: LinearMap.singularValues_of_finrank_le
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
⊢ ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E

Tactic:
have hS : ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E := by
    grind [singularValues_of_finrank_le]
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
hS : ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)

Tactic:
have hT := T.isSymmetric_adjoint_comp_self
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
hS : ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)
h :
  ∀ (i : Fin (finrank 𝕜 E)),
    i ∈ T.singularValues.support.attachFin hS ↔
      Membership.mem (γ := Finset (Fin (finrank 𝕜 E)))
        {i : Fin (finrank 𝕜 E) | Eq.{u_1 + 1} (α := 𝕜) (↑(hT.eigenvalues ⋯ i) : 𝕜) 0}ᶜ i
⊢ T.singularValues.support.attachFin hS = {i : Fin (finrank 𝕜 E) | Eq.{u_1 + 1} (α := 𝕜) (↑(hT.eigenvalues ⋯ i) : 𝕜) 0}ᶜ

Tactic:
ext i
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
hS : ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)
i : Fin (finrank 𝕜 E)
⊢ i ∈ T.singularValues.support.attachFin hS ↔
    Membership.mem (γ := Finset (Fin (finrank 𝕜 E)))
      {i : Fin (finrank 𝕜 E) | Eq.{u_1 + 1} (α := 𝕜) (↑(hT.eigenvalues ⋯ i) : 𝕜) 0}ᶜ i

Tactic:
simp [T.singularValues_fin, T.isPositive_adjoint_comp_self.nonneg_eigenvalues]

Premises used: LinearMap.isPositive_adjoint_comp_self, LinearMap.IsPositive.nonneg_eigenvalues, LinearMap.singularValues_fin
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
hS : ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)
⊢ T.singularValues.support.attachFin hS = {i : Fin (finrank 𝕜 E) | Eq.{u_1 + 1} (α := 𝕜) (↑(hT.eigenvalues ⋯ i) : 𝕜) 0}ᶜ

Tactic:
have : T.singularValues.support.attachFin hS = ({i | hT.eigenvalues rfl i = (0 : 𝕜)} : Finset _)ᶜ
    := by ext i; simp [T.singularValues_fin, T.isPositive_adjoint_comp_self.nonneg_eigenvalues]
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
hS : ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)
this :
  T.singularValues.support.attachFin hS = {i : Fin (finrank 𝕜 E) | Eq.{u_1 + 1} (α := 𝕜) (↑(hT.eigenvalues ⋯ i) : 𝕜) 0}ᶜ
rw : (T.singularValues.support.attachFin hS).card = finrank.{u_1, u_3} 𝕜 ↥T.range
rw₁ :
  Finset.card (α := Fin (finrank 𝕜 E)) {i : Fin (finrank 𝕜 E) | Eq.{u_1 + 1} (α := 𝕜) (↑(hT.eigenvalues ⋯ i) : 𝕜) 0}ᶜ =
    finrank.{u_1, u_3} 𝕜 ↥T.range
rw₂ :
  Fintype.card (Fin (finrank 𝕜 E)) -
      Finset.card (α := Fin (finrank 𝕜 E))
        {i : Fin (finrank 𝕜 E) | Eq.{u_1 + 1} (α := 𝕜) (↑(hT.eigenvalues ⋯ i) : 𝕜) 0} =
    finrank.{u_1, u_3} 𝕜 ↥T.range
rw₃ :
  finrank 𝕜 E -
      Finset.card (α := Fin (finrank 𝕜 E))
        {i : Fin (finrank 𝕜 E) | Eq.{u_1 + 1} (α := 𝕜) (↑(hT.eigenvalues ⋯ i) : 𝕜) 0} =
    finrank.{u_1, u_3} 𝕜 ↥T.range
rw₄ :
  finrank 𝕜 E - finrank.{u_1, u_2} 𝕜 ↥(End.eigenspace ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0) =
    finrank.{u_1, u_3} 𝕜 ↥T.range
rw₅ :
  finrank 𝕜 E - finrank.{u_1, u_2} 𝕜 ↥(ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)) =
    finrank.{u_1, u_3} 𝕜 ↥T.range
rw₆ :
  finrank.{u_1, u_2} 𝕜 ↥(range ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)) +
        finrank.{u_1, u_2} 𝕜 ↥(ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)) -
      finrank.{u_1, u_2} 𝕜 ↥(ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)) =
    finrank.{u_1, u_3} 𝕜 ↥T.range
rw₇ : finrank.{u_1, u_2} 𝕜 ↥(range ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)) = finrank.{u_1, u_3} 𝕜 ↥T.range
rw₈ :
  finrank.{u_1, u_2} 𝕜
      ↥(range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
          ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T)) =
    finrank.{u_1, u_3} 𝕜 ↥T.range
rw₉ rw₁₀ : finrank.{u_1, u_3} 𝕜 ↥T.range = finrank.{u_1, u_3} 𝕜 ↥T.range
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range

Tactic:
rw [← T.singularValues.support.card_attachFin hS, this, Finset.card_compl, Fintype.card_fin,
    hT.card_filter_eigenvalues_eq rfl 0, Module.End.eigenspace_zero,
    ← (T.adjoint ∘ₗ T).finrank_range_add_finrank_ker, add_tsub_cancel_right,
    T.range_adjoint_comp_self, finrank_range_adjoint]

Premises used: Fintype.card_fin, Finset.card_compl, LinearMap.IsSymmetric.card_filter_eigenvalues_eq, Finsupp.support, Finset.card_attachFin, LinearMap.singularValues, LinearMap.comp, LinearMap.finrank_range_adjoint, LinearMap.range_adjoint_comp_self, Module.End.eigenspace_zero, add_tsub_cancel_right, OfNat.ofNat, DFunLike.coe, LinearMap.finrank_range_add_finrank_ker, LinearMap.adjoint, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
a b : ℕ
hl : b ≤ a
ha : a ∈ (↑T.singularValues.support : Set ℕ)
rw :
  ∀ (ha : LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) a : ℝ)),
    LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) b : ℝ)
⊢ b ∈ (↑T.singularValues.support : Set ℕ)

Tactic:
rw [Finset.mem_coe, Finsupp.mem_support_iff, ← singularValues_pos_iff_ne_zero] at ⊢ ha

Premises used: Finsupp.mem_support_iff, LinearMap.singularValues_pos_iff_ne_zero, Finset.mem_coe
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
a b : ℕ
hl : b ≤ a
ha : LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) a : ℝ)
order order₁ order₂ order₃ : ¬LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) b : ℝ) → False
order₄ order₅ order₆ order₇ order₈ order₉ order₁₀ order₁₁ :
  LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) b : ℝ) (0 : ℝ) → False
⊢ LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) b : ℝ)

Tactic:
order [T.singularValues_antitone hl]

Premises used: LinearMap.singularValues_antitone
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
obtain :
  ∀ (n : ℕ) (hn : (↑T.singularValues.support : Set ℕ) = Set.Iio n),
    T.singularValues.support = Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range)
⊢ 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 _))

Premises used: IsLowerSet.eq_univ_or_Iio, LinearMap.isLowerSet_support_singularValues, Or.resolve_left, Set.infinite_univ, Set.Infinite.not_finite
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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 n

Tactic:
rw [← Finset.coe_Iio, Finset.coe_inj, Nat.Iio_eq_range] at hn

Premises used: Finset.coe_inj, Finset.coe_Iio, Nat.Iio_eq_range
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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 = Finset.range n
⊢ T.singularValues.support = Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range)

Tactic:
simp [← card_support_singularValues, hn]

Premises used: LinearMap.card_support_singularValues
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
rw₃ rw₄ : n < 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

Tactic:
rw [singularValues_pos_iff_ne_zero, ← Finsupp.mem_support_iff, support_singularValues,
    Finset.mem_range]

Premises used: Finsupp.mem_support_iff, Finset.mem_range, LinearMap.singularValues_pos_iff_ne_zero, LinearMap.support_singularValues
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
rw : finrank.{u_1, u_3} 𝕜 ↥T.range ∉ Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range)
⊢ Eq (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) (finrank.{u_1, u_3} 𝕜 ↥T.range) : ℝ) (0 : ℝ)

Tactic:
rw [← Finsupp.notMem_support_iff, support_singularValues]

Premises used: Finsupp.notMem_support_iff, LinearMap.support_singularValues
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
⊢ finrank.{u_1, u_3} 𝕜 ↥T.range ∉ Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range)

Tactic:
Finset.notMem_range_self

Premises used: Finset.notMem_range_self
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
⊢ finrank.{u_1, u_3} 𝕜 ↥T.range ∉ Finset.range (finrank.{u_1, u_3} 𝕜 ↥T.range)

Tactic:
exact Finset.notMem_range_self

Premises used: Finset.notMem_range_self
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
rw₃ rw₄ : finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n
⊢ Eq (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ finrank.{u_1, u_3} 𝕜 ↥T.range ≤ n

Tactic:
rw [← Finsupp.notMem_support_iff, support_singularValues, Finset.mem_range, not_lt]

Premises used: Finsupp.notMem_support_iff, Finset.mem_range, not_lt, LinearMap.support_singularValues
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
h :
  ∀ (i : ℕ),
    Eq (α := ℝ) ((singularValues.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) (F := F) 0 : (a : ℕ) → ℝ) i : ℝ)
      ((0 : (a : ℕ) → ℝ) i : ℝ)
⊢ singularValues.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) (F := F) 0 = 0

Tactic:
ext1 i
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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 : ℕ
h : finrank.{u_1, u_3} 𝕜 ↥⊥ ≤ i
⊢ Eq (α := ℝ) ((singularValues.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) (F := F) 0 : (a : ℕ) → ℝ) i : ℝ)
    ((0 : (a : ℕ) → ℝ) i : ℝ)

Tactic:
rw [Finsupp.zero_apply, singularValues_eq_zero_iff_le_finrank_range, range_zero]

Premises used: LinearMap.range_zero, Finsupp.zero_apply, LinearMap.singularValues_eq_zero_iff_le_finrank_range
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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 : ℕ
⊢ finrank.{u_1, u_3} 𝕜 ↥⊥ ≤ i

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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
mpr : T = 0 → T.singularValues = 0
⊢ T.singularValues = 0 ↔ T = 0

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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 : ℝ)
mp₅ mp₆ : Eq (α := ℝ) 0 0
⊢ T = 0

Tactic:
rw [← range_eq_bot, ← Submodule.finrank_eq_zero, ← Nat.le_zero,
      ← singularValues_eq_zero_iff_le_finrank_range, h, Finsupp.zero_apply]

Premises used: Nat.le_zero, LinearMap.range_eq_bot, Submodule.finrank_eq_zero, Finsupp.zero_apply, LinearMap.singularValues_eq_zero_iff_le_finrank_range
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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 = 0
⊢ T.singularValues = 0

Tactic:
h ▸ singularValues_zero

Premises used: LinearMap.singularValues_zero, Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.SingularValues
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 = 0
⊢ T.singularValues = 0

Tactic:
exact h ▸ singularValues_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
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
rwa rwa₁ rwa₂ rwa₃ : ∀ (hw : (T : (a : E) → E) w = μ • w), (T : (a : E) → E) w = μ • w
⊢ (T : (a : E) → E) w = μ • w

Tactic:
rwa [mem_eigenspace_iff] at hw

Premises used: Module.End.mem_eigenspace_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
⊢ (T : (a : E) → E) w = μ • w

Tactic:
have : T w = (μ : 𝕜) • w := by rwa [mem_eigenspace_iff] at hw