awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have hS : ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E
Tactic: have hS : ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E := by
    grind [singularValues_of_finrank_le]
-- 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
hS : ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)
Tactic: have hT := T.isSymmetric_adjoint_comp_self
-- 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
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}ᶜ
have 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 sorry i) : 𝕜) 0}ᶜ i
Tactic: ext i
-- 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
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.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have this : T.singularValues.support.attachFin hS = {i : Fin (finrank 𝕜 E) | Eq.{u_1 + 1} (α := 𝕜) (↑(hT.eigenvalues sorry 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]
-- 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
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}ᶜ
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have rw : (T.singularValues.support.attachFin hS).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]
-- 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
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
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have rw₁ : Finset.card (α := Fin (finrank 𝕜 E)) {i : Fin (finrank 𝕜 E) | Eq.{u_1 + 1} (α := 𝕜) (↑(hT.eigenvalues sorry i) : 𝕜) 0}ᶜ =
  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]
-- 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
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
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have rw₂ : Fintype.card (Fin (finrank 𝕜 E)) -
    Finset.card (α := Fin (finrank 𝕜 E)) {i : Fin (finrank 𝕜 E) | Eq.{u_1 + 1} (α := 𝕜) (↑(hT.eigenvalues sorry i) : 𝕜) 0} =
  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]
-- 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
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
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have rw₃ : finrank 𝕜 E -
    Finset.card (α := Fin (finrank 𝕜 E)) {i : Fin (finrank 𝕜 E) | Eq.{u_1 + 1} (α := 𝕜) (↑(hT.eigenvalues sorry i) : 𝕜) 0} =
  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]
-- 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
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
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have 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
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]
-- 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
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
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have 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
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]
-- 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
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
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have 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
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]
-- 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
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
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have rw₇ : finrank.{u_1, u_2} 𝕜 ↥(range ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)) = 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]
-- 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
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
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have 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
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]
-- 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
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
⊢ T.singularValues.support.card = finrank.{u_1, u_3} 𝕜 ↥T.range
have rw₉ : finrank.{u_1, u_3} 𝕜 ↥T.range = 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]
-- 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
a b : ℕ
hl : b ≤ a
ha : a ∈ (↑T.singularValues.support : Set ℕ)
⊢ b ∈ (↑T.singularValues.support : Set ℕ)
have rw : ∀ (ha : LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) a : ℝ)),
  LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) b : ℝ)
Tactic: rw [Finset.mem_coe, Finsupp.mem_support_iff, ← singularValues_pos_iff_ne_zero] at ⊢ ha
Cleared hypotheses: ha
-- 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
a b : ℕ
hl : b ≤ a
ha : LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) a : ℝ)
⊢ LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) b : ℝ)
have order : ¬LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) b : ℝ) → False
Tactic: order [T.singularValues_antitone hl]
-- 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
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
⊢ LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) b : ℝ)
have order₄ : LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) b : ℝ) (0 : ℝ) → False
Tactic: order [T.singularValues_antitone hl]