awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Semisimple
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite.{u_1, u_2} 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
this : q ⊔ qᗮ = ⊤
rw : (q ⊔ qᗮ) ⊓ p = p
rw₁ : ⊤ ⊓ p = p
rw₂ rw₃ : p = p
⊢ q ⊔ qᗮ ⊓ p = p

Tactic:
rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]

Premises used: top_inf_eq, sup_inf_assoc_of_le
-- Module: Mathlib.Analysis.InnerProductSpace.Semisimple
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite.{u_1, u_2} 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
refine_3 : q ⊔ qᗮ = ⊤
⊢ q ⊔ qᗮ ⊓ p = p

Tactic:
suffices q ⊔ qᗮ = ⊤ by rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]
-- Module: Mathlib.Analysis.InnerProductSpace.Semisimple
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite.{u_1, u_2} 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ Module.Finite.{u_1, u_2} 𝕜 ↥q

Tactic:
replace hp₂ : Module.Finite 𝕜 q := Submodule.finiteDimensional_of_le hq₂
-- Module: Mathlib.Analysis.InnerProductSpace.Semisimple
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
hp₂ : Module.Finite.{u_1, u_2} 𝕜 ↥q
⊢ q ⊔ qᗮ = ⊤

Tactic:
Submodule.sup_orthogonal_of_hasOrthogonalProjection

Premises used: Set.Mem, setOf, Submodule.sup_orthogonal_of_hasOrthogonalProjection
-- Module: Mathlib.Analysis.InnerProductSpace.Semisimple
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
hp₂ : Module.Finite.{u_1, u_2} 𝕜 ↥q
⊢ q ⊔ qᗮ = ⊤

Tactic:
exact Submodule.sup_orthogonal_of_hasOrthogonalProjection

Premises used: Submodule.sup_orthogonal_of_hasOrthogonalProjection
-- 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
i : ℕ
rw :
  LE.le (α := ℝ) 0
    (if h : ∃ (a : Fin (finrank 𝕜 E)), (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i then
      √(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯
          (h.choose (p := fun (a : Fin (finrank 𝕜 E)) ↦ (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i)))
    else 0)
⊢ LE.le (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)

Tactic:
rw [singularValues, Finsupp.embDomain_apply, Finsupp.ofSupportFinite_coe]

Premises used: Finsupp.embDomain_apply, LinearMap.singularValues, Finsupp.ofSupportFinite_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
i : ℕ
pos :
  ∀ (h : ∃ (a : Fin (finrank 𝕜 E)), (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i),
    0 ≤
      √(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯
          (h.choose (p := fun (a : Fin (finrank 𝕜 E)) ↦ (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i)))
neg : (¬∃ (a : Fin (finrank 𝕜 E)), (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i) → LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ) 0
    (if h : ∃ (a : Fin (finrank 𝕜 E)), (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i then
      √(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯
          (h.choose (p := fun (a : Fin (finrank 𝕜 E)) ↦ (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i)))
    else 0)

Tactic:
split_ifs
-- 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
i : ℕ
h : ∃ (a : Fin (finrank 𝕜 E)), (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i
⊢ 0 ≤
    √(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯
        (h.choose (p := fun (a : Fin (finrank 𝕜 E)) ↦ (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i)))

Tactic:
positivity
-- 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
i : ℕ
h : ¬∃ (a : Fin (finrank 𝕜 E)), (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i
⊢ LE.le (α := ℝ) 0 0

Tactic:
positivity
-- 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
i : ℕ
⊢ LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) ↔
    Ne (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)

Tactic:
grind [T.singularValues_nonneg i]

Premises used: LinearMap.singularValues_nonneg
-- 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 : finrank 𝕜 E = n
i : Fin n
subst :
  ∀ (i : Fin (finrank 𝕜 E)),
    (T.singularValues : (a : ℕ) → ℝ) (↑i : ℕ) =
      √(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ i)
⊢ (T.singularValues : (a : ℕ) → ℝ) (↑i : ℕ) =
    √(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ hn i)

Tactic:
subst hn
-- 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
i : Fin (finrank 𝕜 E)
⊢ (T.singularValues : (a : ℕ) → ℝ) (↑i : ℕ) =
    √(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ i)

Tactic:
Finsupp.embDomain_apply_self _ _ i

Premises used: Set.Mem, setOf, Finsupp.embDomain_apply_self, NNReal.toReal
-- 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
i : Fin (finrank 𝕜 E)
⊢ (T.singularValues : (a : ℕ) → ℝ) (↑i : ℕ) =
    √(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ i)

Tactic:
exact Finsupp.embDomain_apply_self _ _ i

Premises used: Finsupp.embDomain_apply_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 : ℕ
hn : finrank 𝕜 E = n
i : ℕ
hi : i < n
⊢ (T.singularValues : (a : ℕ) → ℝ) i =
    √(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ hn (⟨i, hi⟩ : Fin n))

Tactic:
T.singularValues_fin hn ⟨i, hi⟩

Premises used: Set.Mem, setOf, Fin.mk, 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
i : ℕ
hi : finrank 𝕜 E ≤ i
h : i ∉ Set.range (ι := Fin (finrank 𝕜 E)) (⇑Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ)
⊢ Eq (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)

Tactic:
apply Finsupp.embDomain_notin_range

Premises used: Finsupp.embDomain_notin_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
i : ℕ
hi : finrank 𝕜 E ≤ i
⊢ i ∉ Set.range (ι := Fin (finrank 𝕜 E)) (⇑Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ)

Tactic:
simp [hi]
-- 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 : finrank 𝕜 E = n
i : Fin n
⊢ HPow.hPow (α := ℝ) (β := ℕ) ((T.singularValues : (a : ℕ) → ℝ) (↑i : ℕ) : ℝ) 2 =
    IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ hn i

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

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
n : ℕ
hn : finrank 𝕜 E = n
i : ℕ
hi : i < n
⊢ HPow.hPow (α := ℝ) (β := ℕ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) 2 =
    IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ hn ⟨i, hi⟩

Tactic:
T.sq_singularValues_fin hn ⟨i, hi⟩

Premises used: Set.Mem, setOf, Fin.mk, LinearMap.sq_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
n : ℕ
hn : n < finrank 𝕜 E
⊢ End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)
    (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯
          (⟨n, hn⟩ : Fin (finrank 𝕜 E))) :
      𝕜)

Tactic:
T.isSymmetric_adjoint_comp_self.hasEigenvalue_eigenvalues rfl ⟨n, hn⟩

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
n : ℕ
hn : n < finrank 𝕜 E
h :
  HPow.hPow (α := 𝕜) (β := ℕ) (↑((T.singularValues : (a : ℕ) → ℝ) n) : 𝕜) 2 =
    (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯
          (⟨n, hn⟩ : Fin (finrank 𝕜 E))) :
      𝕜)
⊢ End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)
    (HPow.hPow (α := 𝕜) (β := ℕ) (↑((T.singularValues : (a : ℕ) → ℝ) n) : 𝕜) 2)

Tactic:
convert! T.isSymmetric_adjoint_comp_self.hasEigenvalue_eigenvalues rfl ⟨n, hn⟩ using 1

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
n : ℕ
hn : n < finrank 𝕜 E
⊢ HPow.hPow (α := 𝕜) (β := ℕ) (↑((T.singularValues : (a : ℕ) → ℝ) n) : 𝕜) 2 =
    (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯
          (⟨n, hn⟩ : Fin (finrank 𝕜 E))) :
      𝕜)

Tactic:
simp [← T.sq_singularValues_fin]

Premises used: LinearMap.sq_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
i j : ℕ
hij : i ≤ j
pos :
  ∀ (hj : finrank 𝕜 E ≤ j),
    LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
neg :
  ∀ (hj : j < finrank 𝕜 E),
    LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
⊢ LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)

Tactic:
by_cases! hj : finrank 𝕜 E ≤ j

Premises used: Module.finrank
-- 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
i j : ℕ
hij : i ≤ j
hj : finrank 𝕜 E ≤ j
⊢ LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)

Tactic:
simpa [T.singularValues_of_finrank_le hj] using T.singularValues_nonneg i

Premises used: LinearMap.singularValues_nonneg, 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
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
rw :
  IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ (⟨j, hj⟩ : Fin (finrank 𝕜 E)) ≤
    IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ (⟨i, ⋯⟩ : Fin (finrank 𝕜 E))
⊢ HPow.hPow (α := ℝ) (β := ℕ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) 2 ≤
    HPow.hPow (α := ℝ) (β := ℕ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) 2

Tactic:
rw [T.sq_singularValues_fin rfl ⟨j, hj⟩, T.sq_singularValues_fin rfl ⟨i, hij.trans_lt hj⟩]

Premises used: Fin.mk, LinearMap.sq_singularValues_fin, LE.le.trans_lt, 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
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
⊢ IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ (⟨j, hj⟩ : Fin (finrank 𝕜 E)) ≤
    IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ (⟨i, ⋯⟩ : Fin (finrank 𝕜 E))

Tactic:
T.isSymmetric_adjoint_comp_self.eigenvalues_antitone rfl hij

Premises used: LinearMap.isSymmetric_adjoint_comp_self, rfl, LinearMap.IsSymmetric.eigenvalues_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
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
⊢ IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ (⟨j, hj⟩ : Fin (finrank 𝕜 E)) ≤
    IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ (⟨i, ⋯⟩ : Fin (finrank 𝕜 E))

Tactic:
exact T.isSymmetric_adjoint_comp_self.eigenvalues_antitone rfl hij

Premises used: LinearMap.isSymmetric_adjoint_comp_self, rfl, LinearMap.IsSymmetric.eigenvalues_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
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
⊢ HPow.hPow (α := ℝ) (β := ℕ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) 2 ≤
    HPow.hPow (α := ℝ) (β := ℕ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) 2

Tactic:
have : (T.singularValues j : ℝ) ^ 2 ≤ (T.singularValues i : ℝ) ^ 2 := by
    rw [T.sq_singularValues_fin rfl ⟨j, hj⟩, T.sq_singularValues_fin rfl ⟨i, hij.trans_lt hj⟩]
    exact T.isSymmetric_adjoint_comp_self.eigenvalues_antitone rfl hij
-- 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
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
this :
  HPow.hPow (α := ℝ) (β := ℕ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) 2 ≤
    HPow.hPow (α := ℝ) (β := ℕ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) 2
⊢ LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)

Tactic:
le_of_sq_le_sq this (T.singularValues_nonneg i)

Premises used: LinearMap.singularValues_nonneg, le_of_sq_le_sq
-- 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
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
this :
  HPow.hPow (α := ℝ) (β := ℕ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) 2 ≤
    HPow.hPow (α := ℝ) (β := ℕ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) 2
⊢ LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)

Tactic:
exact le_of_sq_le_sq this (T.singularValues_nonneg i)

Premises used: LinearMap.singularValues_nonneg, le_of_sq_le_sq
-- 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
⊢ ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) = ⊥ ↔
    ¬End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0

Tactic:
have := (adjoint T ∘ₗ T).not_hasEigenvalue_zero_tfae.out 4 0
-- 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
rw :
  End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0 ↔
    ¬∀ i < finrank 𝕜 E, LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F) ↔
    ∀ i < finrank 𝕜 E, LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)

Tactic:
rw [← adjoint_comp_self_injective_iff, ← coe_comp, ← ker_eq_bot, ← not_iff_not, this.not_left]

Premises used: not_iff_not, LinearMap.ker_eq_bot, LinearMap.adjoint_comp_self_injective_iff, Iff.not_left, LinearMap.coe_comp
-- 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
push :
  End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0 ↔
    ∃ i < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
⊢ End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0 ↔
    ¬∀ i < finrank 𝕜 E, LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)

Tactic:
push Not

Premises used: Not
-- 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
mp :
  End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0 →
    ∃ i < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
mpr :
  (∃ i < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)) →
    End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0
⊢ End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0 ↔
    ∃ i < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (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
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
mp :
  ∀ (i : Fin (finrank 𝕜 E))
    (hi :
      Eq.{u_1 + 1} (α := 𝕜) (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ i) : 𝕜)
        0),
    ∃ i < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
⊢ ∃ i < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)

Tactic:
obtain ⟨i, hi⟩ := T.isSymmetric_adjoint_comp_self.exists_eigenvalues_eq rfl h

Premises used: LinearMap.isSymmetric_adjoint_comp_self, LinearMap.IsSymmetric.exists_eigenvalues_eq, rfl