awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (hypothesis)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
i j : n
hdiag : ∀ (i : n), A i i = 0
h1 :
  LE.le (α := 𝕜) 0
    ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
      (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
        star xi * A i_1 j * xj)
⊢ A i j = 0 i j
have h2 : LE.le (α := 𝕜) 0
  ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
    (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
      star xi * (-A) i_1 j * xj)
Tactic: have h2 := h₂.2 (.single i 1 + .single j (A j i))
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
i j : n
hdiag : ∀ (i : n), A i i = 0
h1 :
  LE.le (α := 𝕜) 0
    ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
      (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
        star xi * A i_1 j * xj)
h2 :
  LE.le (α := 𝕜) 0
    ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
      (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
        star xi * (-A) i_1 j * xj)
⊢ A i j = 0 i j
have a : ∀ (hdiag : True) (h1 : 0 ≤ A i j * star (A i j) + A i j * star (A i j))
  (h2 : A i j * star (A i j) + A i j * star (A i j) ≤ 0), A i j = 0
Tactic: simp [Finsupp.sum_add_index, mul_add, add_mul,
      -neg_add_rev, hdiag, ← h₁.1.apply j i, -RCLike.star_def] at *
Cleared hypotheses: hdiag, h1, h2
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
⊢ A = 0
have a : ∀ (i j : n), A i j = 0 i j
Tactic: classical
  ext i j
  have hdiag i : A i i = 0 :=
    le_antisymm (by simpa using h₂.diag_nonneg) (by simpa using h₁.diag_nonneg)
  have h1 := h₁.2 (.single i 1 + .single j (A j i))
  have h2 := h₂.2 (.single i 1 + .single j (A j i))
  simp [Finsupp.sum_add_index, mul_add, add_mul,
      -neg_add_rev, hdiag, ← h₁.1.apply j i, -RCLike.star_def] at *
  simpa using le_antisymm h2 h1
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
a : ∀ (i j : n), A i j = 0 i j
⊢ A = 0
have a₁ : ∀ (i j : n) (hdiag : ∀ (i : n), A i i = 0), A i j = 0 i j
Tactic: classical
  ext i j
  have hdiag i : A i i = 0 :=
    le_antisymm (by simpa using h₂.diag_nonneg) (by simpa using h₁.diag_nonneg)
  have h1 := h₁.2 (.single i 1 + .single j (A j i))
  have h2 := h₂.2 (.single i 1 + .single j (A j i))
  simp [Finsupp.sum_add_index, mul_add, add_mul,
      -neg_add_rev, hdiag, ← h₁.1.apply j i, -RCLike.star_def] at *
  simpa using le_antisymm h2 h1
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
a : ∀ (i j : n), A i j = 0 i j
a₁ : ∀ (i j : n) (hdiag : ∀ (i : n), A i i = 0), A i j = 0 i j
⊢ A = 0
have a₂ : ∀ (i j : n) (hdiag : ∀ (i : n), A i i = 0)
  (h1 :
    LE.le (α := 𝕜) 0
      ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
        (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
          star xi * A i_1 j * xj)),
  A i j = 0 i j
Tactic: classical
  ext i j
  have hdiag i : A i i = 0 :=
    le_antisymm (by simpa using h₂.diag_nonneg) (by simpa using h₁.diag_nonneg)
  have h1 := h₁.2 (.single i 1 + .single j (A j i))
  have h2 := h₂.2 (.single i 1 + .single j (A j i))
  simp [Finsupp.sum_add_index, mul_add, add_mul,
      -neg_add_rev, hdiag, ← h₁.1.apply j i, -RCLike.star_def] at *
  simpa using le_antisymm h2 h1
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
a : ∀ (i j : n), A i j = 0 i j
a₁ : ∀ (i j : n) (hdiag : ∀ (i : n), A i i = 0), A i j = 0 i j
a₂ :
  ∀ (i j : n) (hdiag : ∀ (i : n), A i i = 0)
    (h1 :
      LE.le (α := 𝕜) 0
        ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
          (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
            star xi * A i_1 j * xj)),
    A i j = 0 i j
⊢ A = 0
have a₃ : ∀ (i j : n) (hdiag : ∀ (i : n), A i i = 0)
  (h1 :
    LE.le (α := 𝕜) 0
      ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
        (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
          star xi * A i_1 j * xj))
  (h2 :
    LE.le (α := 𝕜) 0
      ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
        (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
          star xi * (-A) i_1 j * xj)),
  A i j = 0 i j
Tactic: classical
  ext i j
  have hdiag i : A i i = 0 :=
    le_antisymm (by simpa using h₂.diag_nonneg) (by simpa using h₁.diag_nonneg)
  have h1 := h₁.2 (.single i 1 + .single j (A j i))
  have h2 := h₂.2 (.single i 1 + .single j (A j i))
  simp [Finsupp.sum_add_index, mul_add, add_mul,
      -neg_add_rev, hdiag, ← h₁.1.apply j i, -RCLike.star_def] at *
  simpa using le_antisymm h2 h1
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
a : ∀ (i j : n), A i j = 0 i j
a₁ : ∀ (i j : n) (hdiag : ∀ (i : n), A i i = 0), A i j = 0 i j
a₂ :
  ∀ (i j : n) (hdiag : ∀ (i : n), A i i = 0)
    (h1 :
      LE.le (α := 𝕜) 0
        ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
          (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
            star xi * A i_1 j * xj)),
    A i j = 0 i j
a₃ :
  ∀ (i j : n) (hdiag : ∀ (i : n), A i i = 0)
    (h1 :
      LE.le (α := 𝕜) 0
        ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
          (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
            star xi * A i_1 j * xj))
    (h2 :
      LE.le (α := 𝕜) 0
        ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
          (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
            star xi * (-A) i_1 j * xj)),
    A i j = 0 i j
⊢ A = 0
have a₄ : ∀ (i j : n) (hdiag : True) (h1 : 0 ≤ A i j * star (A i j) + A i j * star (A i j))
  (h2 : A i j * star (A i j) + A i j * star (A i j) ≤ 0), A i j = 0
Tactic: classical
  ext i j
  have hdiag i : A i i = 0 :=
    le_antisymm (by simpa using h₂.diag_nonneg) (by simpa using h₁.diag_nonneg)
  have h1 := h₁.2 (.single i 1 + .single j (A j i))
  have h2 := h₂.2 (.single i 1 + .single j (A j i))
  simp [Finsupp.sum_add_index, mul_add, add_mul,
      -neg_add_rev, hdiag, ← h₁.1.apply j i, -RCLike.star_def] at *
  simpa using le_antisymm h2 h1
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
x x_1 : Matrix n n 𝕜
h : x ≤ x_1
x_2 : Matrix n n 𝕜
⊢ x + x_2 ≤ x_1 + x_2
have rwa : (x_1 + x_2 - (x + x_2)).PosSemidef
Tactic: rwa [le_iff, add_sub_add_right_eq_sub]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
x x_1 : Matrix n n 𝕜
h : x ≤ x_1
x_2 : Matrix n n 𝕜
rwa : (x_1 + x_2 - (x + x_2)).PosSemidef
⊢ x + x_2 ≤ x_1 + x_2
have rwa₁ : (x_1 - x).PosSemidef
Tactic: rwa [le_iff, add_sub_add_right_eq_sub]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : 0 ≤ A
⊢ ∀ x ∈ quasispectrum ℝ A, 0 ≤ x
have simp : ∀ a ∈ spectrum ℝ A, 0 ≤ a
Tactic: simp only [quasispectrum_eq_spectrum_union_zero ℝ A, Set.union_singleton, Set.mem_insert_iff,
      forall_eq_or_imp, le_refl, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : 0 ≤ A
x : ℝ
hx : x ∈ spectrum ℝ A
⊢ 0 ≤ x
have obtain : ∀ (i : n) (hx : sorry.eigenvalues i ∈ spectrum ℝ A), 0 ≤ sorry.eigenvalues i
Tactic: obtain ⟨i, rfl⟩ := Set.ext_iff.mp
      hA.posSemidef.1.spectrum_real_eq_range_eigenvalues x |>.mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : 0 ≤ A
⊢ ∀ x ∈ quasispectrum ℝ A, 0 ≤ x
have simp : ∀ a ∈ spectrum ℝ A, 0 ≤ a
Tactic: classical
    simp only [quasispectrum_eq_spectrum_union_zero ℝ A, Set.union_singleton, Set.mem_insert_iff,
      forall_eq_or_imp, le_refl, true_and]
    intro x hx
    obtain ⟨i, rfl⟩ := Set.ext_iff.mp
      hA.posSemidef.1.spectrum_real_eq_range_eigenvalues x |>.mp hx
    exact hA.posSemidef.eigenvalues_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : 0 ≤ A
simp simp₁ : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ A), 0 ≤ x
⊢ ∀ x ∈ quasispectrum ℝ A, 0 ≤ x
have simp₂ : ∀ (i : n) (hx : sorry.eigenvalues i ∈ spectrum ℝ A), 0 ≤ sorry.eigenvalues i
Tactic: classical
    simp only [quasispectrum_eq_spectrum_union_zero ℝ A, Set.union_singleton, Set.mem_insert_iff,
      forall_eq_or_imp, le_refl, true_and]
    intro x hx
    obtain ⟨i, rfl⟩ := Set.ext_iff.mp
      hA.posSemidef.1.spectrum_real_eq_range_eigenvalues x |>.mp hx
    exact hA.posSemidef.eigenvalues_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : 0 ≤ A
⊢ ∃ (s : Matrix n n 𝕜), A = star s * s
have obtain : ∀ (X : Matrix n n 𝕜) (hX : IsSelfAdjoint X) (hA : 0 ≤ X * X), ∃ (s : Matrix n n 𝕜), X * X = star s * s
Tactic: obtain ⟨X, hX, -, rfl⟩ :=
        sub_zero A ▸ CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts hA.isHermitian
          (QuasispectrumRestricts.nnreal_of_nonneg hA.nonneg)
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : 0 ≤ A
⊢ ∃ (s : Matrix n n 𝕜), A = star s * s
have obtain : ∀ (X : Matrix n n 𝕜) (hX : IsSelfAdjoint X) (hA : 0 ≤ X * X), ∃ (s : Matrix n n 𝕜), X * X = star s * s
Tactic: classical
      obtain ⟨X, hX, -, rfl⟩ :=
        sub_zero A ▸ CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts hA.isHermitian
          (QuasispectrumRestricts.nnreal_of_nonneg hA.nonneg)
      exact ⟨X, hX.star_eq.symm ▸ rfl⟩
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ (CFC.sqrt A)⁻¹ = CFC.sqrt A⁻¹
have rw : CFC.sqrt A⁻¹ = (CFC.sqrt A)⁻¹
Tactic: rw [eq_comm, CFC.sqrt_eq_iff _ _ hA.inv.nonneg (CFC.sqrt_nonneg A).posSemidef.inv.nonneg, ← sq,
    inv_pow', CFC.sq_sqrt A]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
rw : CFC.sqrt A⁻¹ = (CFC.sqrt A)⁻¹
⊢ (CFC.sqrt A)⁻¹ = CFC.sqrt A⁻¹
have rw₁ : (CFC.sqrt A)⁻¹ * (CFC.sqrt A)⁻¹ = A⁻¹
Tactic: rw [eq_comm, CFC.sqrt_eq_iff _ _ hA.inv.nonneg (CFC.sqrt_nonneg A).posSemidef.inv.nonneg, ← sq,
    inv_pow', CFC.sq_sqrt A]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
rw : CFC.sqrt A⁻¹ = (CFC.sqrt A)⁻¹
rw₁ : (CFC.sqrt A)⁻¹ * (CFC.sqrt A)⁻¹ = A⁻¹
⊢ (CFC.sqrt A)⁻¹ = CFC.sqrt A⁻¹
have rw₂ : HPow.hPow (β := ℕ) (CFC.sqrt A)⁻¹ 2 = A⁻¹
Tactic: rw [eq_comm, CFC.sqrt_eq_iff _ _ hA.inv.nonneg (CFC.sqrt_nonneg A).posSemidef.inv.nonneg, ← sq,
    inv_pow', CFC.sq_sqrt A]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
rw : CFC.sqrt A⁻¹ = (CFC.sqrt A)⁻¹
rw₁ : (CFC.sqrt A)⁻¹ * (CFC.sqrt A)⁻¹ = A⁻¹
rw₂ : HPow.hPow (β := ℕ) (CFC.sqrt A)⁻¹ 2 = A⁻¹
⊢ (CFC.sqrt A)⁻¹ = CFC.sqrt A⁻¹
have rw₃ : (HPow.hPow (β := ℕ) (CFC.sqrt A) 2)⁻¹ = A⁻¹
Tactic: rw [eq_comm, CFC.sqrt_eq_iff _ _ hA.inv.nonneg (CFC.sqrt_nonneg A).posSemidef.inv.nonneg, ← sq,
    inv_pow', CFC.sq_sqrt A]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
rw : CFC.sqrt A⁻¹ = (CFC.sqrt A)⁻¹
rw₁ : (CFC.sqrt A)⁻¹ * (CFC.sqrt A)⁻¹ = A⁻¹
rw₂ : HPow.hPow (β := ℕ) (CFC.sqrt A)⁻¹ 2 = A⁻¹
rw₃ : (HPow.hPow (β := ℕ) (CFC.sqrt A) 2)⁻¹ = A⁻¹
⊢ (CFC.sqrt A)⁻¹ = CFC.sqrt A⁻¹
have rw₄ : A⁻¹ = A⁻¹
Tactic: rw [eq_comm, CFC.sqrt_eq_iff _ _ hA.inv.nonneg (CFC.sqrt_nonneg A).posSemidef.inv.nonneg, ← sq,
    inv_pow', CFC.sq_sqrt A]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
⊢ star x ⬝ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0
have refine : ∀ (h : star x ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h ▸ dotProduct_zero _⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
h : star x ⬝ᵥ A *ᵥ x = 0
⊢ A *ᵥ x = 0
have obtain : ∀ (B : Matrix n n 𝕜) (hA : (star B * B).PosSemidef) (h : star x ⬝ᵥ (star B * B) *ᵥ x = 0), (star B * B) *ᵥ x = 0
Tactic: obtain ⟨B, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hA.nonneg
Cleared hypotheses: A, hA, h
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
x : n → 𝕜
B : Matrix n n 𝕜
hA : (star B * B).PosSemidef
h : star x ⬝ᵥ (star B * B) *ᵥ x = 0
⊢ (star B * B) *ᵥ x = 0
have simp_rw : ∀ (h : B *ᵥ x = 0), Bᴴ *ᵥ B *ᵥ x = 0
Tactic: simp_rw [← Matrix.mulVec_mulVec, dotProduct_mulVec _ _ (B *ᵥ x), star_eq_conjTranspose,
    vecMul_conjTranspose, star_star, dotProduct_star_self_eq_zero] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
x : n → 𝕜
B : Matrix n n 𝕜
hA : (star B * B).PosSemidef
h : B *ᵥ x = 0
⊢ Bᴴ *ᵥ B *ᵥ x = 0
have rw : Bᴴ *ᵥ 0 = 0
Tactic: rw [h, mulVec_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
x : n → 𝕜
B : Matrix n n 𝕜
hA : (star B * B).PosSemidef
h : B *ᵥ x = 0
rw : Bᴴ *ᵥ 0 = 0
⊢ Bᴴ *ᵥ B *ᵥ x = 0
have rw₁ : Eq (α := n → 𝕜) 0 0
Tactic: rw [h, mulVec_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
⊢ star x ⬝ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0
have refine : ∀ (h : star x ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
Tactic: classical
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ dotProduct_zero _⟩
  obtain ⟨B, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hA.nonneg
  simp_rw [← Matrix.mulVec_mulVec, dotProduct_mulVec _ _ (B *ᵥ x), star_eq_conjTranspose,
    vecMul_conjTranspose, star_star, dotProduct_star_self_eq_zero] at h ⊢
  rw [h, mulVec_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
refine : ∀ (h : star x ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
⊢ star x ⬝ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0
have refine₁ : ∀ (B : Matrix n n 𝕜) (hA : (star B * B).PosSemidef) (h : star x ⬝ᵥ (star B * B) *ᵥ x = 0), (star B * B) *ᵥ x = 0
Tactic: classical
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ dotProduct_zero _⟩
  obtain ⟨B, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hA.nonneg
  simp_rw [← Matrix.mulVec_mulVec, dotProduct_mulVec _ _ (B *ᵥ x), star_eq_conjTranspose,
    vecMul_conjTranspose, star_star, dotProduct_star_self_eq_zero] at h ⊢
  rw [h, mulVec_zero]
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
refine : ∀ (h : star x ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
refine₁ :
  ∀ (B : Matrix n n 𝕜) (hA : (star B * B).PosSemidef) (h : star x ⬝ᵥ (star B * B) *ᵥ x = 0), (star B * B) *ᵥ x = 0
⊢ star x ⬝ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0
have refine₂ : ∀ (B : Matrix n n 𝕜) (hA : (star B * B).PosSemidef) (h : B *ᵥ x = 0), Bᴴ *ᵥ B *ᵥ x = 0
Tactic: classical
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ dotProduct_zero _⟩
  obtain ⟨B, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hA.nonneg
  simp_rw [← Matrix.mulVec_mulVec, dotProduct_mulVec _ _ (B *ᵥ x), star_eq_conjTranspose,
    vecMul_conjTranspose, star_star, dotProduct_star_self_eq_zero] at h ⊢
  rw [h, mulVec_zero]
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ (CFC.sqrt A).det = RCLike.sqrt A.det
have rw : (sorry.cfc fun (x : ℝ) ↦ (↑((NNReal.sqrt : (a : NNReal) → NNReal) x.toNNReal) : ℝ)).det =
  (↑√((RCLike.re : (a : 𝕜) → ℝ) A.det) : 𝕜)
Tactic: rw [CFC.sqrt_eq_cfc, cfc_nnreal_eq_real _ A, hA.1.cfc_eq, RCLike.sqrt_of_nonneg hA.det_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ (⋯.cfc fun (x : ℝ) ↦ (↑((NNReal.sqrt : (a : NNReal) → NNReal) x.toNNReal) : ℝ)).det =
    (↑√((RCLike.re : (a : 𝕜) → ℝ) A.det) : 𝕜)
have simp : Eq.{u_1 + 1} (α := 𝕜) (↑(∏ i : n, √(max (sorry.eigenvalues i) 0)) : 𝕜) (↑(∏ i : n, √(sorry.eigenvalues i)) : 𝕜)
Tactic: simp only [IsHermitian.cfc, Real.coe_sqrt, Real.coe_toNNReal', det_map, det_diagonal,
    Function.comp_apply, hA.isHermitian.det_eq_prod_eigenvalues, ← RCLike.ofReal_prod,
    RCLike.ofReal_re, Real.sqrt_prod _ fun _ _ ↦ hA.eigenvalues_nonneg _]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
⊢ A.PosSemidef ↔ A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}
have refine_1 : ∀ (h : A.PosSemidef), ∀ a ∈ spectrum 𝕜 A, Membership.mem (γ := Set 𝕜) {a : 𝕜 | 0 ≤ a} a
Tactic: refine ⟨fun h => ⟨h.isHermitian, fun a => ?_⟩, fun ⟨h1, h2⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
refine_1 : ∀ (h : A.PosSemidef), ∀ a ∈ spectrum 𝕜 A, Membership.mem (γ := Set 𝕜) {a : 𝕜 | 0 ≤ a} a
⊢ A.PosSemidef ↔ A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}
have refine_2 : A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a} →
  ∀ (h1 : A.IsHermitian) (h2 : spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}), A.PosSemidef
Tactic: refine ⟨fun h => ⟨h.isHermitian, fun a => ?_⟩, fun ⟨h1, h2⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
h : A.PosSemidef
a : 𝕜
⊢ a ∈ spectrum 𝕜 A → Membership.mem (γ := Set 𝕜) {a : 𝕜 | 0 ≤ a} a
have refine_1 : ∀ (x : n) (h : (↑(sorry.eigenvalues x) : 𝕜) = a), 0 ≤ a
Tactic: simp only [h.isHermitian.spectrum_eq_image_range, Set.mem_image, Set.mem_range,
      exists_exists_eq_and, Set.mem_setOf_eq, forall_exists_index]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
h : A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}
h1 : A.IsHermitian
h2 : spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}
⊢ A.PosSemidef
have refine_2 : 0 ≤ h1.eigenvalues
Tactic: rw [h1.posSemidef_iff_eigenvalues_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
x : Matrix n n 𝕜
hx : x.PosSemidef
⊢ x.PosDef ↔ IsUnit x
have refine : ∀ (h : IsUnit x) (v : n → 𝕜) (hv : v ≠ 0), 0 < star v ⬝ᵥ x *ᵥ v
Tactic: refine ⟨fun h => h.isUnit, fun h => .of_dotProduct_mulVec_pos hx.1 fun v hv => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
x : Matrix n n 𝕜
hx : x.PosSemidef
h : IsUnit x
v : n → 𝕜
hv : v ≠ 0
⊢ 0 < star v ⬝ᵥ x *ᵥ v
have obtain : ∀ (y : Matrix n n 𝕜) (hx : (star y * y).PosSemidef) (h : IsUnit (star y * y)), 0 < star v ⬝ᵥ (star y * y) *ᵥ v
Tactic: obtain ⟨y, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx.nonneg
Cleared hypotheses: x, hx, h
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
hv : v ≠ 0
y : Matrix n n 𝕜
hx : (star y * y).PosSemidef
h : IsUnit (star y * y)
⊢ 0 < star v ⬝ᵥ (star y * y) *ᵥ v
have simp_rw : y *ᵥ v ≠ 0
Tactic: simp_rw [dotProduct_mulVec, ← vecMul_vecMul, star_eq_conjTranspose, ← star_mulVec,
    ← dotProduct_mulVec, dotProduct_star_self_pos_iff]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
hv : v ≠ 0
y : Matrix n n 𝕜
hx : (star y * y).PosSemidef
h : IsUnit (star y * y)
⊢ y *ᵥ v ≠ 0
have contrapose : ∀ (hv : y *ᵥ v = 0), v = 0
Tactic: contrapose hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
y : Matrix n n 𝕜
hx : (star y * y).PosSemidef
h : IsUnit (star y * y)
hv : y *ᵥ v = 0
⊢ v = 0
have rw : Eq (α := n → 𝕜) (((yᴴ * y).mulVecLin : (a : n → 𝕜) → n → 𝕜) v : n → 𝕜) (0 : n → 𝕜)
Tactic: rw [← map_eq_zero_iff (f := (yᴴ * y).mulVecLin) (mulVec_injective_iff_isUnit.mpr h),
    mulVecLin_apply, ← mulVec_mulVec, hv, mulVec_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
y : Matrix n n 𝕜
hx : (star y * y).PosSemidef
h : IsUnit (star y * y)
hv : y *ᵥ v = 0
rw : Eq (α := n → 𝕜) (((yᴴ * y).mulVecLin : (a : n → 𝕜) → n → 𝕜) v : n → 𝕜) (0 : n → 𝕜)
⊢ v = 0
have rw₁ : (yᴴ * y) *ᵥ v = 0
Tactic: rw [← map_eq_zero_iff (f := (yᴴ * y).mulVecLin) (mulVec_injective_iff_isUnit.mpr h),
    mulVecLin_apply, ← mulVec_mulVec, hv, mulVec_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
y : Matrix n n 𝕜
hx : (star y * y).PosSemidef
h : IsUnit (star y * y)
hv : y *ᵥ v = 0
rw : Eq (α := n → 𝕜) (((yᴴ * y).mulVecLin : (a : n → 𝕜) → n → 𝕜) v : n → 𝕜) (0 : n → 𝕜)
rw₁ : (yᴴ * y) *ᵥ v = 0
⊢ v = 0
have rw₂ : yᴴ *ᵥ y *ᵥ v = 0
Tactic: rw [← map_eq_zero_iff (f := (yᴴ * y).mulVecLin) (mulVec_injective_iff_isUnit.mpr h),
    mulVecLin_apply, ← mulVec_mulVec, hv, mulVec_zero]