awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAs :
  PosDef (n := ↥x.support)
    (A.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
      (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))
hBs :
  PosDef (n := ↥x.support)
    (B.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
      (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))
y : ↥x.support → 𝕜
hy : y ≠ 0
⊢ 0 <
    star y ⬝ᵥ
      A.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
            (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)) ⊙
          B.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
            (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)) *ᵥ
        y
have rw : 0 <
  star (diagonal y).vec ⬝ᵥ
    kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2)
        (A.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
          (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))
        (B.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
          (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))) *ᵥ
      (diagonal y).vec
Tactic: rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
⊢ LT.lt (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
have hAB : PosDef (n := ↥x.support)
  ((A ⊙ B).submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
    (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))
Tactic: have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosDef := by
    have hAs : (A.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hA.submatrix Subtype.coe_injective
    have hBs : (B.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hB.submatrix Subtype.coe_injective
    rw [submatrix_hadamard, posDef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y hy ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_pos <| by simpa
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAB :
  PosDef (n := ↥x.support)
    ((A ⊙ B).submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
      (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))
⊢ LT.lt (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
have simp_rw : LT.lt.{u_1} (α := 𝕜) 0
  (∑ x_1 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_1 : ι) ↦ x_1 ∈ x.support) x),
    ∑ x_2 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_2 : ι) ↦ x_2 ∈ x.support) x),
      HMul.hMul (β := 𝕜)
        (HMul.hMul (α := 𝕜)
          ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
              ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_1 : 𝕜) :
            𝕜)
          (A (↑x_1 : ι) (↑x_2 : ι) * B (↑x_1 : ι) (↑x_2 : ι)))
        ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_2 : 𝕜))
Tactic: simp_rw [RCLike.star_def, hadamard_apply, Finsupp.sum,
    ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAB :
  PosDef (n := ↥x.support)
    ((A ⊙ B).submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
      (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))
⊢ LT.lt.{u_1} (α := 𝕜) 0
    (∑ x_1 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_1 : ι) ↦ x_1 ∈ x.support) x),
      ∑ x_2 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_2 : ι) ↦ x_2 ∈ x.support) x),
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜)
            ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
                ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_1 : 𝕜) :
              𝕜)
            (A (↑x_1 : ι) (↑x_2 : ι) * B (↑x_1 : ι) (↑x_2 : ι)))
          ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_2 : 𝕜))
have refine : Ne (α := Finsupp.{u_3, u_1} (↥x.support) 𝕜) (Finsupp.subtypeDomain (fun (x_1 : ι) ↦ x_1 ∈ x.support) x) 0
Tactic: refine hAB.2 ?_
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
⊢ (A ⊙ B).PosDef
have refine : ∀ (x : ι →₀ 𝕜) (hx : x ≠ 0),
  LT.lt (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
Tactic: classical
  refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x hx ↦ ?_⟩
  have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosDef := by
    have hAs : (A.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hA.submatrix Subtype.coe_injective
    have hBs : (B.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hB.submatrix Subtype.coe_injective
    rw [submatrix_hadamard, posDef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y hy ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_pos <| by simpa
  simp_rw [RCLike.star_def, hadamard_apply, Finsupp.sum,
    ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain]
  refine hAB.2 ?_
  simpa [← Finsupp.support_nonempty_iff] using Finsupp.support_nonempty_iff.mpr hx
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
refine :
  ∀ (x : ι →₀ 𝕜) (hx : x ≠ 0),
    LT.lt (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
⊢ (A ⊙ B).PosDef
have refine₁ : ∀ (x : ι →₀ 𝕜) (hx : x ≠ 0)
  (hAB :
    PosDef (n := ↥x.support)
      ((A ⊙ B).submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
        (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))),
  LT.lt (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
Tactic: classical
  refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x hx ↦ ?_⟩
  have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosDef := by
    have hAs : (A.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hA.submatrix Subtype.coe_injective
    have hBs : (B.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hB.submatrix Subtype.coe_injective
    rw [submatrix_hadamard, posDef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y hy ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_pos <| by simpa
  simp_rw [RCLike.star_def, hadamard_apply, Finsupp.sum,
    ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain]
  refine hAB.2 ?_
  simpa [← Finsupp.support_nonempty_iff] using Finsupp.support_nonempty_iff.mpr hx
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
refine :
  ∀ (x : ι →₀ 𝕜) (hx : x ≠ 0),
    LT.lt (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
refine₁ :
  ∀ (x : ι →₀ 𝕜) (hx : x ≠ 0)
    (hAB :
      PosDef (n := ↥x.support)
        ((A ⊙ B).submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
          (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))),
    LT.lt (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
⊢ (A ⊙ B).PosDef
have refine₂ : ∀ (x : ι →₀ 𝕜) (hx : x ≠ 0)
  (hAB :
    PosDef (n := ↥x.support)
      ((A ⊙ B).submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
        (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))),
  LT.lt.{u_1} (α := 𝕜) 0
    (∑ x_1 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_1 : ι) ↦ x_1 ∈ x.support) x),
      ∑ x_2 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_2 : ι) ↦ x_2 ∈ x.support) x),
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜)
            ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
                ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_1 : 𝕜) :
              𝕜)
            (A (↑x_1 : ι) (↑x_2 : ι) * B (↑x_1 : ι) (↑x_2 : ι)))
          ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_2 : 𝕜))
Tactic: classical
  refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x hx ↦ ?_⟩
  have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosDef := by
    have hAs : (A.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hA.submatrix Subtype.coe_injective
    have hBs : (B.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hB.submatrix Subtype.coe_injective
    rw [submatrix_hadamard, posDef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y hy ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_pos <| by simpa
  simp_rw [RCLike.star_def, hadamard_apply, Finsupp.sum,
    ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain]
  refine hAB.2 ?_
  simpa [← Finsupp.support_nonempty_iff] using Finsupp.support_nonempty_iff.mpr hx
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
refine :
  ∀ (x : ι →₀ 𝕜) (hx : x ≠ 0),
    LT.lt (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
refine₁ :
  ∀ (x : ι →₀ 𝕜) (hx : x ≠ 0)
    (hAB :
      PosDef (n := ↥x.support)
        ((A ⊙ B).submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
          (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))),
    LT.lt (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
refine₂ :
  ∀ (x : ι →₀ 𝕜) (hx : x ≠ 0)
    (hAB :
      PosDef (n := ↥x.support)
        ((A ⊙ B).submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
          (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))),
    LT.lt.{u_1} (α := 𝕜) 0
      (∑ x_1 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_1 : ι) ↦ x_1 ∈ x.support) x),
        ∑ x_2 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_2 : ι) ↦ x_2 ∈ x.support) x),
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜)
              ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
                  ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_1 : 𝕜) :
                𝕜)
              (A (↑x_1 : ι) (↑x_2 : ι) * B (↑x_1 : ι) (↑x_2 : ι)))
            ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_2 : 𝕜))
⊢ (A ⊙ B).PosDef
have refine₃ : ∀ (x : ι →₀ 𝕜) (hx : x ≠ 0)
  (hAB :
    PosDef (n := ↥x.support)
      ((A ⊙ B).submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
        (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))),
  Ne (α := Finsupp.{u_3, u_1} (↥x.support) 𝕜) (Finsupp.subtypeDomain (fun (x_1 : ι) ↦ x_1 ∈ x.support) x) 0
Tactic: classical
  refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x hx ↦ ?_⟩
  have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosDef := by
    have hAs : (A.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hA.submatrix Subtype.coe_injective
    have hBs : (B.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hB.submatrix Subtype.coe_injective
    rw [submatrix_hadamard, posDef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y hy ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_pos <| by simpa
  simp_rw [RCLike.star_def, hadamard_apply, Finsupp.sum,
    ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain]
  refine hAB.2 ?_
  simpa [← Finsupp.support_nonempty_iff] using Finsupp.support_nonempty_iff.mpr 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
M : Matrix n n 𝕜
hM : M.PosDef
x : Matrix n n 𝕜
hx : inner 𝕜 x x = 0
⊢ x = 0
have obtain : ∀ (y : Matrix n n 𝕜) (hy : IsUnit y) (hM : (star y * y).PosDef) (hx : inner 𝕜 x x = 0), x = 0
Tactic: obtain ⟨y, hy, rfl⟩ := CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self.mp
        hM.isStrictlyPositive
Cleared hypotheses: M, hM, hx
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (hypothesis)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
x y : Matrix n n 𝕜
hy : IsUnit y
hM : (star y * y).PosDef
__spread.0 : PreInnerProductSpace.Core 𝕜 (Matrix n n 𝕜) := ⋯.matrixPreInnerProductSpace
hx : (x * (star y * y) * xᴴ).trace = 0
⊢ x = 0
have hx₁ : y * xᴴ = 0
Tactic: rw [← mul_assoc, ← conjTranspose_conjTranspose x, star_eq_conjTranspose, ← conjTranspose_mul,
        conjTranspose_conjTranspose, mul_assoc, trace_conjTranspose_mul_self_eq_zero_iff] at hx
Cleared hypotheses: 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
x y : Matrix n n 𝕜
hy : IsUnit y
hM : (star y * y).PosDef
__spread.0 : PreInnerProductSpace.Core 𝕜 (Matrix n n 𝕜) := ⋯.matrixPreInnerProductSpace
hx : y * xᴴ = 0
⊢ x = 0
have lift : ∀ (y : (Matrix n n 𝕜)ˣ) (hM : (star (↑y : Matrix n n 𝕜) * (↑y : Matrix n n 𝕜)).PosDef)
  (hx : (↑y : Matrix n n 𝕜) * xᴴ = 0), x = 0
Tactic: lift y to (Matrix n n 𝕜)ˣ using hy
Cleared hypotheses: y, hy, hM, __spread.0, 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
M : Matrix n n 𝕜
hM : M.PosDef
x : Matrix n n 𝕜
hx : inner 𝕜 x x = 0
⊢ x = 0
have obtain : ∀ (y : Matrix n n 𝕜) (hy : IsUnit y) (hM : (star y * y).PosDef) (hx : inner 𝕜 x x = 0), x = 0
Tactic: classical
      obtain ⟨y, hy, rfl⟩ := CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self.mp
        hM.isStrictlyPositive
      simp +instances only at hx
      rw [← mul_assoc, ← conjTranspose_conjTranspose x, star_eq_conjTranspose, ← conjTranspose_mul,
        conjTranspose_conjTranspose, mul_assoc, trace_conjTranspose_mul_self_eq_zero_iff] at hx
      lift y to (Matrix n n 𝕜)ˣ using hy
      simpa [← mul_assoc] using congr(y⁻¹ * $hx)
Cleared hypotheses: M, hM, 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
M : Matrix n n 𝕜
hM : M.PosDef
x : Matrix n n 𝕜
hx : inner 𝕜 x x = 0
obtain : ∀ (y : Matrix n n 𝕜) (hy : IsUnit y) (hM : (star y * y).PosDef) (hx : inner 𝕜 x x = 0), x = 0
⊢ x = 0
have obtain₁ : ∀ (y : Matrix n n 𝕜) (hy : IsUnit y) (hM : (star y * y).PosDef) (hx : (x * (star y * y) * xᴴ).trace = 0), x = 0
Tactic: classical
      obtain ⟨y, hy, rfl⟩ := CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self.mp
        hM.isStrictlyPositive
      simp +instances only at hx
      rw [← mul_assoc, ← conjTranspose_conjTranspose x, star_eq_conjTranspose, ← conjTranspose_mul,
        conjTranspose_conjTranspose, mul_assoc, trace_conjTranspose_mul_self_eq_zero_iff] at hx
      lift y to (Matrix n n 𝕜)ˣ using hy
      simpa [← mul_assoc] using congr(y⁻¹ * $hx)
Cleared hypotheses: M, hM, 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
M : Matrix n n 𝕜
hM : M.PosDef
x : Matrix n n 𝕜
hx : inner 𝕜 x x = 0
obtain : ∀ (y : Matrix n n 𝕜) (hy : IsUnit y) (hM : (star y * y).PosDef) (hx : inner 𝕜 x x = 0), x = 0
obtain₁ :
  ∀ (y : Matrix n n 𝕜) (hy : IsUnit y) (hM : (star y * y).PosDef) (hx : (x * (star y * y) * xᴴ).trace = 0), x = 0
⊢ x = 0
have obtain₂ : ∀ (y : Matrix n n 𝕜) (hy : IsUnit y) (hM : (star y * y).PosDef) (hx : y * xᴴ = 0), x = 0
Tactic: classical
      obtain ⟨y, hy, rfl⟩ := CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self.mp
        hM.isStrictlyPositive
      simp +instances only at hx
      rw [← mul_assoc, ← conjTranspose_conjTranspose x, star_eq_conjTranspose, ← conjTranspose_mul,
        conjTranspose_conjTranspose, mul_assoc, trace_conjTranspose_mul_self_eq_zero_iff] at hx
      lift y to (Matrix n n 𝕜)ˣ using hy
      simpa [← mul_assoc] using congr(y⁻¹ * $hx)
Cleared hypotheses: M, hM, 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
M : Matrix n n 𝕜
hM : M.PosDef
x : Matrix n n 𝕜
hx : inner 𝕜 x x = 0
obtain : ∀ (y : Matrix n n 𝕜) (hy : IsUnit y) (hM : (star y * y).PosDef) (hx : inner 𝕜 x x = 0), x = 0
obtain₁ :
  ∀ (y : Matrix n n 𝕜) (hy : IsUnit y) (hM : (star y * y).PosDef) (hx : (x * (star y * y) * xᴴ).trace = 0), x = 0
obtain₂ : ∀ (y : Matrix n n 𝕜) (hy : IsUnit y) (hM : (star y * y).PosDef) (hx : y * xᴴ = 0), x = 0
⊢ x = 0
have obtain₃ : ∀ (y : (Matrix n n 𝕜)ˣ) (hM : (star (↑y : Matrix n n 𝕜) * (↑y : Matrix n n 𝕜)).PosDef)
  (hx : (↑y : Matrix n n 𝕜) * xᴴ = 0), x = 0
Tactic: classical
      obtain ⟨y, hy, rfl⟩ := CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self.mp
        hM.isStrictlyPositive
      simp +instances only at hx
      rw [← mul_assoc, ← conjTranspose_conjTranspose x, star_eq_conjTranspose, ← conjTranspose_mul,
        conjTranspose_conjTranspose, mul_assoc, trace_conjTranspose_mul_self_eq_zero_iff] at hx
      lift y to (Matrix n n 𝕜)ˣ using hy
      simpa [← mul_assoc] using congr(y⁻¹ * $hx)
Cleared hypotheses: M, hM, hx
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [hA.spectral_theorem]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ A.PosSemidef ↔ 0 ≤ hA.eigenvalues
have conv_lhs : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: conv_lhs => rw [hA.spectral_theorem]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.PosSemidef
⊢ 0 ≤ A.det
have rw : LE.le.{u_3} (α := 𝕜) 0 (∏ i : n, (↑(sorry.eigenvalues i) : 𝕜))
Tactic: rw [hA.isHermitian.det_eq_prod_eigenvalues]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
| A.trace = 0
have rw : ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → Eq.{u_3 + 1} (α := 𝕜) ((RCLike.ofReal ∘ sorry.eigenvalues) i) 0
Tactic: rw [hA.1.spectral_theorem, conjStarAlgAut_apply, trace_mul_cycle, coe_star_mul_self,
    one_mul, trace_diagonal, Finset.sum_eq_zero_iff_of_nonneg (by simp [hA.eigenvalues_nonneg])]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ A.trace = 0 ↔ A = 0
have conv_lhs : A.trace = 0 ↔ A = 0
Tactic: classical
  conv_lhs => rw [hA.1.spectral_theorem, conjStarAlgAut_apply, trace_mul_cycle, coe_star_mul_self,
    one_mul, trace_diagonal, Finset.sum_eq_zero_iff_of_nonneg (by simp [hA.eigenvalues_nonneg])]
  simp [← hA.isHermitian.eigenvalues_eq_zero_iff, funext_iff]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
conv_lhs : A.trace = 0 ↔ A = 0
⊢ A.trace = 0 ↔ A = 0
have conv_lhs₁ : (∀ (i : n),
    Membership.mem (γ := Finset n) Finset.univ i → Eq.{u_3 + 1} (α := 𝕜) ((RCLike.ofReal ∘ sorry.eigenvalues) i) 0) ↔
  A = 0
Tactic: classical
  conv_lhs => rw [hA.1.spectral_theorem, conjStarAlgAut_apply, trace_mul_cycle, coe_star_mul_self,
    one_mul, trace_diagonal, Finset.sum_eq_zero_iff_of_nonneg (by simp [hA.eigenvalues_nonneg])]
  simp [← hA.isHermitian.eigenvalues_eq_zero_iff, funext_iff]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ A.PosDef ↔ ∀ (i : n), 0 < hA.eigenvalues i
have conv_lhs : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: conv_lhs => rw [hA.spectral_theorem]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.PosDef
⊢ 0 < A.det
have rw : LT.lt.{u_3} (α := 𝕜) 0 (∏ i : n, (↑(sorry.eigenvalues i) : 𝕜))
Tactic: rw [hA.isHermitian.det_eq_prod_eigenvalues]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.PosDef
⊢ LT.lt.{u_3} (α := 𝕜) 0 (∏ i : n, (↑(⋯.eigenvalues i) : 𝕜))
have h0 : ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → LT.lt.{u_3} (α := 𝕜) 0 (↑(sorry.eigenvalues i) : 𝕜)
Tactic: apply Finset.prod_pos
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (M *ᵥ x ⬝ᵥ star y) = M *ᵥ y ⬝ᵥ star x
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star y ⬝ᵥ M *ᵥ x) = M *ᵥ y ⬝ᵥ star x
Tactic: rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star,
      star_mulVec, dotProduct_comm (M *ᵥ y), dotProduct_mulVec, hM.isHermitian.eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star y ⬝ᵥ M *ᵥ x) = M *ᵥ y ⬝ᵥ star x
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (M *ᵥ x ⬝ᵥ star y) = M *ᵥ y ⬝ᵥ star x
have rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
Tactic: rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star,
      star_mulVec, dotProduct_comm (M *ᵥ y), dotProduct_mulVec, hM.isHermitian.eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star y ⬝ᵥ M *ᵥ x) = M *ᵥ y ⬝ᵥ star x
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (M *ᵥ x ⬝ᵥ star y) = M *ᵥ y ⬝ᵥ star x
have rw₂ : star (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
Tactic: rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star,
      star_mulVec, dotProduct_comm (M *ᵥ y), dotProduct_mulVec, hM.isHermitian.eq]