awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
f : OfKernel K
h :
  Eq (α := X → V)
    ((ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
            (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
              (kerFun K x) :
          (a : OfKernel K) → X → V)
        f :
      X → V)
    (0 : X → V)
ff : H₀ K
zero : ⟪(↑0 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
⊢ ⟪(↑ff : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
have single_add : ∀ (i : X × V) (a : 𝕜) (f_1 : X × V →₀ 𝕜),
  i ∉ f_1.support →
    a ≠ 0 →
      ⟪(↑f_1 : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0 →
        ⟪(↑(Finsupp.single i a + f_1) : UniformSpace.Completion (H₀ K)), f⟫_𝕜 = 0
Tactic: induction ff using Finsupp.induction with
    | zero =>
      have : @UniformSpace.Completion.coe' (H₀ K) PseudoMetricSpace.toUniformSpace 0 = 0 := rfl
      simp [this]
    | single_add i a =>
    simp only [UniformSpace.Completion.coe_add, inner_add_left, *, add_zero]
    rw [← UniformSpace.Completion.coe_toComplL (𝕜 := 𝕜)]
    have := (ext_iff_inner_left 𝕜).mp (congrFun h i.1) i.2
    have := by simpa [OfKernel.kerFun, adjoint_inner_right] using this
    rw [← mul_zero (conj a), ← this, ← inner_smul_left]
    refine (ext_iff_inner_right 𝕜).mp ?_ f
    simp [← UniformSpace.Completion.coe_toComplL (𝕜 := 𝕜),
      ← map_smul, -SeparationQuotient.mkCLM_apply, -UniformSpace.Completion.coe_toComplL]
Cleared hypotheses: ff
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_4 : Fact K.PosSemidef
⊢ kernel (OfKernel K) = K
have a : ∀ (x y : X) (v : V), Eq (α := V) ((kernel (OfKernel K) x y : (a : V) → V) v : V) ((K x y : (a : V) → V) v : V)
Tactic: ext x y v
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Reproducing (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_4 : Fact K.PosSemidef
x y : X
v : V
⊢ Eq (α := V) ((kernel (OfKernel K) x y : (a : V) → V) v : V) ((K x y : (a : V) → V) v : V)
have a : ∀ (w : V), ⟪(kernel (OfKernel K) x y : (a : V) → V) v, w⟫_𝕜 = ⟪(K x y : (a : V) → V) v, w⟫_𝕜
Tactic: refine ext_inner_right 𝕜 fun w ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Semisimple (goal)
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
⊢ T.IsFinitelySemisimple
have refine_1 : ∀ (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), qᗮ ∈ T.invtSubmodule
Tactic: refine Module.End.isFinitelySemisimple_iff.mpr fun p hp₁ hp₂ q hq₁ hq₂ ↦
    ⟨qᗮ ⊓ p, inf_le_right, Module.End.invtSubmodule.inf_mem ?_ hp₁, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Semisimple (goal)
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
refine_1 :
  ∀ (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), qᗮ ∈ T.invtSubmodule
⊢ T.IsFinitelySemisimple
have refine_2 : ∀ (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), Disjoint q (qᗮ ⊓ p)
Tactic: refine Module.End.isFinitelySemisimple_iff.mpr fun p hp₁ hp₂ q hq₁ hq₂ ↦
    ⟨qᗮ ⊓ p, inf_le_right, Module.End.invtSubmodule.inf_mem ?_ hp₁, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Semisimple (goal)
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
refine_1 :
  ∀ (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), qᗮ ∈ T.invtSubmodule
refine_2 :
  ∀ (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), Disjoint q (qᗮ ⊓ p)
⊢ T.IsFinitelySemisimple
have refine_3 : ∀ (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), q ⊔ qᗮ ⊓ p = p
Tactic: refine Module.End.isFinitelySemisimple_iff.mpr fun p hp₁ hp₂ q hq₁ hq₂ ↦
    ⟨qᗮ ⊓ p, inf_le_right, Module.End.invtSubmodule.inf_mem ?_ hp₁, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Semisimple (goal)
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ᗮ = ⊤
⊢ q ⊔ qᗮ ⊓ p = p
have rw : (q ⊔ qᗮ) ⊓ p = p
Tactic: rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Semisimple (goal)
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
⊢ q ⊔ qᗮ ⊓ p = p
have rw₁ : ⊤ ⊓ p = p
Tactic: rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Semisimple (goal)
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
⊢ q ⊔ qᗮ ⊓ p = p
have rw₂ : p = p
Tactic: rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Semisimple (goal)
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
⊢ q ⊔ qᗮ ⊓ p = p
have refine_3 : q ⊔ qᗮ = ⊤
Tactic: suffices q ⊔ qᗮ = ⊤ by rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Semisimple (hypothesis)
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
⊢ q ⊔ qᗮ = ⊤
have hp₃ : Module.Finite.{u_1, u_2} 𝕜 ↥q
Tactic: replace hp₂ : Module.Finite 𝕜 q := Submodule.finiteDimensional_of_le hq₂
Cleared hypotheses: hp₂
-- 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
i : ℕ
⊢ LE.le (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
have 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) sorry sorry
        (h.choose (p := fun (a : Fin (finrank 𝕜 E)) ↦ (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i)))
  else 0)
Tactic: rw [singularValues, Finsupp.embDomain_apply, Finsupp.ofSupportFinite_coe]
-- 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
i : ℕ
⊢ 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)
have 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) sorry sorry
        (h.choose (p := fun (a : Fin (finrank 𝕜 E)) ↦ (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i)))
Tactic: split_ifs
-- 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
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)))
⊢ 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)
have neg : (¬∃ (a : Fin (finrank 𝕜 E)), (Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ) a = i) → LE.le (α := ℝ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
hn : finrank 𝕜 E = n
i : Fin n
⊢ (T.singularValues : (a : ℕ) → ℝ) (↑i : ℕ) =
    √(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ hn i)
have subst : ∀ (i : Fin (finrank 𝕜 E)),
  (T.singularValues : (a : ℕ) → ℝ) (↑i : ℕ) =
    √(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) sorry sorry i)
Tactic: subst hn
Cleared hypotheses: n, hn, i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
i : ℕ
hi : finrank 𝕜 E ≤ i
⊢ Eq (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
have h : i ∉ Set.range (ι := Fin (finrank 𝕜 E)) (⇑Fin.valEmbedding : (a : Fin (finrank 𝕜 E)) → ℕ)
Tactic: apply Finsupp.embDomain_notin_range
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
hn : n < finrank 𝕜 E
⊢ End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T)
    (HPow.hPow (α := 𝕜) (β := ℕ) (↑((T.singularValues : (a : ℕ) → ℝ) n) : 𝕜) 2)
have h : HPow.hPow (α := 𝕜) (β := ℕ) (↑((T.singularValues : (a : ℕ) → ℝ) n) : 𝕜) 2 =
  (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) sorry sorry (⟨n, hn⟩ : Fin (finrank 𝕜 E))) :
    𝕜)
Tactic: convert! T.isSymmetric_adjoint_comp_self.hasEigenvalue_eigenvalues rfl ⟨n, hn⟩ using 1
-- 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
i j : ℕ
hij : i ≤ j
⊢ LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
have pos : ∀ (hj : finrank 𝕜 E ≤ j),
  LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
Tactic: by_cases! hj : finrank 𝕜 E ≤ j
-- 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
i j : ℕ
hij : i ≤ j
pos :
  ∀ (hj : finrank 𝕜 E ≤ j),
    LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
⊢ LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
have neg : ∀ (hj : j < finrank 𝕜 E),
  LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
Tactic: by_cases! hj : finrank 𝕜 E ≤ j
-- 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
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
⊢ HPow.hPow (α := ℝ) (β := ℕ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) 2 ≤
    HPow.hPow (α := ℝ) (β := ℕ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) 2
have rw : IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) sorry sorry (⟨j, hj⟩ : Fin (finrank 𝕜 E)) ≤
  IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) sorry sorry (⟨i, sorry⟩ : Fin (finrank 𝕜 E))
Tactic: rw [T.sq_singularValues_fin rfl ⟨j, hj⟩, T.sq_singularValues_fin rfl ⟨i, hij.trans_lt hj⟩]
-- 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
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
⊢ LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) j : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
have this : 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
-- 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
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F) ↔
    ∀ i < finrank 𝕜 E, LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
have this : 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
-- 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
this :
  ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) = ⊥ ↔
    ¬End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F) ↔
    ∀ i < finrank 𝕜 E, LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
have rw : End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0 ↔
  ¬∀ 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]
-- 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
this :
  ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) = ⊥ ↔
    ¬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, LT.lt (α := ℝ) (0 : ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ)
have push : End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0 ↔
  ∃ i < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
Tactic: push Not
-- 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
this :
  ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) = ⊥ ↔
    ¬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 : ℝ)
have mp : End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0 →
  ∃ i < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
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 : ℝ)
⊢ End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0 ↔
    ∃ i < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
have mpr : (∃ i < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)) →
  End.HasEigenvalue ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.SingularValues (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
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 < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
have mp : ∀ (i : Fin (finrank 𝕜 E))
  (hi :
    Eq.{u_1 + 1} (α := 𝕜) (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) sorry sorry 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
-- 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
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
⊢ ∃ i < finrank 𝕜 E, LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) i : ℝ) (0 : ℝ)
have right : LE.le (α := ℝ) ((T.singularValues : (a : ℕ) → ℝ) (↑i : ℕ) : ℝ) (0 : ℝ)
Tactic: use i, i.isLt
-- 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
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) 0
have h₁ : Eq.{u_1 + 1} (α := 𝕜) 0
  (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) sorry sorry (⟨i, h⟩ : Fin (finrank 𝕜 E))) :
    𝕜)
Tactic: convert! T.isSymmetric_adjoint_comp_self.hasEigenvalue_eigenvalues rfl ⟨i, h⟩
-- 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
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
    (↑(IsSymmetric.eigenvalues (T := (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) T ∘ₗ T) ⋯ ⋯ (⟨i, h⟩ : Fin (finrank 𝕜 E))) :
      𝕜)
have h₁ : Eq.{u_1 + 1} (α := 𝕜) 0 (↑(HPow.hPow (α := ℝ) (β := ℕ) 0 2) : 𝕜)
Tactic: rw [← sq_singularValues_of_lt, le_antisymm hz (T.singularValues_nonneg i)]