awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Matrix.Order
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 : 𝕜))
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
⊢ (A ⊙ B).PosDef

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

Premises used: RCLike.star_def, Finsupp.sum, Finset.subtype_mem_eq_attach, Matrix.hadamard_apply, Finsupp.support_nonempty_iff, Finsupp.subtypeDomain_apply, Finsupp.support_subtypeDomain
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst : Fintype n
inst_1 : Semiring α
inst_2 : RCLike 𝕜
inst_3 : Module α 𝕜
⊢ Eq (α := Matrix n n 𝕜 →ₗ[α] 𝕜) (PositiveLinearMap.toLinearMap (tracePositiveLinearMap n α 𝕜)) (traceLinearMap n α 𝕜)

Tactic:
rfl

Premises used: Matrix.traceLinearMap, rfl
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
n : Type u_3
α : Type u_4
𝕜 : Type u_5
inst : Fintype n
inst_1 : Semiring α
inst_2 : RCLike 𝕜
inst_3 : Module α 𝕜
x : Matrix n n 𝕜
⊢ (tracePositiveLinearMap n α 𝕜 : (a : Matrix n n 𝕜) → 𝕜) x = x.trace

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Matrix.trace, Finset.sum, rfl
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
M : Matrix n n 𝕜
hM : M.PosSemidef
x x_1 : Matrix n n 𝕜
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x * M * x_1ᴴ).trace = (x_1 * M * xᴴ).trace

Tactic:
simp only [mul_assoc, starRingEnd_apply, ← trace_conjTranspose, conjTranspose_mul,
      conjTranspose_conjTranspose, hM.isHermitian.eq]

Premises used: Matrix.PosSemidef.isHermitian, Matrix.IsHermitian.eq, mul_assoc, starRingEnd_apply, Matrix.trace_conjTranspose, Matrix.conjTranspose_conjTranspose, Matrix.conjTranspose_mul
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
M : Matrix n n 𝕜
hM : M.PosSemidef
⊢ ∀ (x y z : Matrix n n 𝕜), (z * M * (x + y)ᴴ).trace = (z * M * xᴴ).trace + (z * M * yᴴ).trace

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
M : Matrix n n 𝕜
hM : M.PosSemidef
⊢ ∀ (x y : Matrix n n 𝕜) (r : 𝕜),
    (y * M * (r • x)ᴴ).trace = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) (y * M * xᴴ).trace

Tactic:
simp
-- Module: Mathlib.Analysis.Matrix.Order
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

Tactic:
obtain ⟨y, hy, rfl⟩ := CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self.mp
        hM.isStrictlyPositive

Premises used: Matrix.PosDef.isStrictlyPositive, Iff.mp, CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self, rfl
-- Module: Mathlib.Analysis.Matrix.Order
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
⊢ 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

Premises used: Matrix.star_eq_conjTranspose, mul_assoc, Matrix.trace_conjTranspose_mul_self_eq_zero_iff, Matrix.conjTranspose_conjTranspose, Matrix.conjTranspose_mul
-- Module: Mathlib.Analysis.Matrix.Order
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
⊢ IsUnit y

Tactic:
hy
-- Module: Mathlib.Analysis.Matrix.Order
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
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
⊢ x = 0

Tactic:
lift y to (Matrix n n 𝕜)ˣ using hy

Premises used: Matrix
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
x : Matrix n n 𝕜
y : (Matrix n n 𝕜)ˣ
hM : (star (↑y : Matrix n n 𝕜) * (↑y : Matrix n n 𝕜)).PosDef
__spread.0 : PreInnerProductSpace.Core 𝕜 (Matrix n n 𝕜) := ⋯.matrixPreInnerProductSpace
hx : (↑y : Matrix n n 𝕜) * xᴴ = 0
⊢ x = 0

Tactic:
simpa [← mul_assoc] using congr(y⁻¹ * $hx)

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Matrix.Order
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
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
⊢ 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)

Premises used: Matrix.star_eq_conjTranspose, Matrix, mul_assoc, Matrix.trace_conjTranspose_mul_self_eq_zero_iff, Matrix.conjTranspose_conjTranspose, Matrix.conjTranspose_mul, rfl
-- Module: Mathlib.Analysis.Matrix.PosDef
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
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [hA.spectral_theorem]

Premises used: Matrix.IsHermitian.spectral_theorem
-- Module: Mathlib.Analysis.Matrix.PosDef
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
conv_lhs : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ A.PosSemidef ↔ 0 ≤ hA.eigenvalues

Tactic:
conv_lhs => rw [hA.spectral_theorem]

Premises used: Matrix.IsHermitian.spectral_theorem
-- Module: Mathlib.Analysis.Matrix.PosDef
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)

Tactic:
simp [isUnit_coe.posSemidef_star_right_conjugate_iff, posSemidef_diagonal_iff, Pi.le_def]

Premises used: Matrix.IsUnit.posSemidef_star_right_conjugate_iff, Matrix.posSemidef_diagonal_iff, Pi.le_def, Unitary.isUnit_coe
-- Module: Mathlib.Analysis.Matrix.PosDef
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
i : n
⊢ 0 ≤ ⋯.eigenvalues i

Tactic:
hA.isHermitian.posSemidef_iff_eigenvalues_nonneg.mp hA _

Premises used: Matrix.PosSemidef.isHermitian, Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg, Iff.mp
-- Module: Mathlib.Analysis.Matrix.PosDef
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
⊢ LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (star x ⬝ᵥ A *ᵥ x) : ℝ)

Tactic:
RCLike.nonneg_iff.mp (hA.dotProduct_mulVec_nonneg _) |>.1

Premises used: RCLike.nonneg_iff, Matrix.PosSemidef.dotProduct_mulVec_nonneg, And.left, Iff.mp
-- Module: Mathlib.Analysis.Matrix.PosDef
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
rw : LE.le.{u_3} (α := 𝕜) 0 (∏ i : n, (↑(⋯.eigenvalues i) : 𝕜))
⊢ 0 ≤ A.det

Tactic:
rw [hA.isHermitian.det_eq_prod_eigenvalues]

Premises used: Matrix.PosSemidef.isHermitian, Matrix.IsHermitian.det_eq_prod_eigenvalues
-- Module: Mathlib.Analysis.Matrix.PosDef
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
i : n
h : Membership.mem (γ := Finset n) Finset.univ i
⊢ LE.le.{u_3} (α := 𝕜) 0 (↑(⋯.eigenvalues i) : 𝕜)

Tactic:
simpa using hA.eigenvalues_nonneg i

Premises used: Matrix.PosSemidef.eigenvalues_nonneg
-- Module: Mathlib.Analysis.Matrix.PosDef
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
⊢ LE.le.{u_3} (α := 𝕜) 0 (∏ i : n, (↑(⋯.eigenvalues i) : 𝕜))

Tactic:
exact Finset.prod_nonneg fun i _ ↦ by simpa using hA.eigenvalues_nonneg i

Premises used: Finset.prod_nonneg
-- Module: Mathlib.Analysis.Matrix.PosDef
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → LE.le.{u_3} (α := 𝕜) 0 ((RCLike.ofReal ∘ ⋯.eigenvalues) i)

Tactic:
simp [hA.eigenvalues_nonneg]

Premises used: Matrix.PosSemidef.eigenvalues_nonneg
-- Module: Mathlib.Analysis.Matrix.PosDef
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
rw :
  ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → Eq.{u_3 + 1} (α := 𝕜) ((RCLike.ofReal ∘ ⋯.eigenvalues) i) 0
| A.trace = 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])]

Premises used: Finset.sum_eq_zero_iff_of_nonneg, Matrix.trace_diagonal, Unitary.conjStarAlgAut_apply, Matrix.IsHermitian.spectral_theorem, And.left, Matrix.trace_mul_cycle, Unitary.coe_star_mul_self, one_mul
-- Module: Mathlib.Analysis.Matrix.PosDef
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ (∀ (i : n),
      Membership.mem (γ := Finset n) Finset.univ i → Eq.{u_3 + 1} (α := 𝕜) ((RCLike.ofReal ∘ ⋯.eigenvalues) i) 0) ↔
    A = 0

Tactic:
simp [← hA.isHermitian.eigenvalues_eq_zero_iff, funext_iff]

Premises used: Matrix.PosSemidef.isHermitian, funext_iff, Matrix.IsHermitian.eigenvalues_eq_zero_iff
-- Module: Mathlib.Analysis.Matrix.PosDef
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
conv_lhs₁ conv_lhs₂ :
  (∀ (i : n),
      Membership.mem (γ := Finset n) Finset.univ i → Eq.{u_3 + 1} (α := 𝕜) ((RCLike.ofReal ∘ ⋯.eigenvalues) i) 0) ↔
    A = 0
⊢ 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]

Premises used: Finset.sum_eq_zero_iff_of_nonneg, funext_iff, Matrix.trace_diagonal, Unitary.conjStarAlgAut_apply, Matrix.trace_mul_cycle, Unitary.coe_star_mul_self, one_mul
-- Module: Mathlib.Analysis.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A : Matrix m n 𝕜
inst_3 : DecidableEq n
i : n
⊢ 0 ≤ IsHermitian.eigenvalues.{u_3, u_2} (𝕜 := 𝕜) (A := Aᴴ * A) ⋯ i

Tactic:
(posSemidef_conjTranspose_mul_self _).eigenvalues_nonneg _

Premises used: Matrix.posSemidef_conjTranspose_mul_self, Matrix.PosSemidef.eigenvalues_nonneg
-- Module: Mathlib.Analysis.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A : Matrix m n 𝕜
inst_3 : DecidableEq m
i : m
⊢ 0 ≤ IsHermitian.eigenvalues.{u_3, u_1} (𝕜 := 𝕜) (A := A * Aᴴ) ⋯ i

Tactic:
(posSemidef_self_mul_conjTranspose _).eigenvalues_nonneg _

Premises used: Matrix.posSemidef_self_mul_conjTranspose, Matrix.PosSemidef.eigenvalues_nonneg
-- Module: Mathlib.Analysis.Matrix.PosDef
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
conv_lhs : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ A.PosDef ↔ ∀ (i : n), 0 < hA.eigenvalues i

Tactic:
conv_lhs => rw [hA.spectral_theorem]

Premises used: Matrix.IsHermitian.spectral_theorem
-- Module: Mathlib.Analysis.Matrix.PosDef
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)

Tactic:
simp [isUnit_coe.posDef_star_right_conjugate_iff]

Premises used: Unitary.isUnit_coe, Matrix.IsUnit.posDef_star_right_conjugate_iff
-- Module: Mathlib.Analysis.Matrix.PosDef
Goal:
n : Type u_2
𝕜 : Type u_3
inst : Fintype n
inst_1 : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosDef
x : n → 𝕜
hx : x ≠ 0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (star x ⬝ᵥ A *ᵥ x) : ℝ)

Tactic:
RCLike.pos_iff.mp (hA.dotProduct_mulVec_pos hx) |>.1

Premises used: RCLike.pos_iff, And.left, Iff.mp, Matrix.PosDef.dotProduct_mulVec_pos
-- Module: Mathlib.Analysis.Matrix.PosDef
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
i : n
⊢ 0 < ⋯.eigenvalues i

Tactic:
hA.isHermitian.posDef_iff_eigenvalues_pos.mp hA i

Premises used: Iff.mp, Matrix.IsHermitian.posDef_iff_eigenvalues_pos, Matrix.PosDef.isHermitian
-- Module: Mathlib.Analysis.Matrix.PosDef
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
rw : LT.lt.{u_3} (α := 𝕜) 0 (∏ i : n, (↑(⋯.eigenvalues i) : 𝕜))
⊢ 0 < A.det

Tactic:
rw [hA.isHermitian.det_eq_prod_eigenvalues]

Premises used: Matrix.IsHermitian.det_eq_prod_eigenvalues, Matrix.PosDef.isHermitian
-- Module: Mathlib.Analysis.Matrix.PosDef
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
h0 : ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → LT.lt.{u_3} (α := 𝕜) 0 (↑(⋯.eigenvalues i) : 𝕜)
⊢ LT.lt.{u_3} (α := 𝕜) 0 (∏ i : n, (↑(⋯.eigenvalues i) : 𝕜))

Tactic:
apply Finset.prod_pos

Premises used: Finset.prod_pos
-- Module: Mathlib.Analysis.Matrix.PosDef
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
i : n
h0 : Membership.mem (γ := Finset n) Finset.univ i → LT.lt.{u_3} (α := 𝕜) 0 (↑(⋯.eigenvalues i) : 𝕜)
⊢ Membership.mem (γ := Finset n) Finset.univ i → LT.lt.{u_3} (α := 𝕜) 0 (↑(⋯.eigenvalues i) : 𝕜)

Tactic:
_
-- Module: Mathlib.Analysis.Matrix.PosDef
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
i : n
h : Membership.mem (γ := Finset n) Finset.univ i
⊢ LT.lt.{u_3} (α := 𝕜) 0 (↑(⋯.eigenvalues i) : 𝕜)

Tactic:
simpa using hA.eigenvalues_pos i

Premises used: Matrix.PosDef.eigenvalues_pos
-- Module: Mathlib.Analysis.Matrix.PosDef
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
rw₂ : star (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
rw₃ : star (M *ᵥ x) ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x
rw₄ : star x ᵥ* Mᴴ ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x
rw₅ : star x ᵥ* Mᴴ ⬝ᵥ y = star x ⬝ᵥ M *ᵥ y
rw₆ : star x ᵥ* Mᴴ ⬝ᵥ y = star x ᵥ* M ⬝ᵥ y
rw₇ rw₈ : star x ᵥ* M ⬝ᵥ y = star x ᵥ* M ⬝ᵥ y
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (M *ᵥ x ⬝ᵥ star 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]

Premises used: Matrix.PosSemidef.isHermitian, Matrix.IsHermitian.eq, star_star, Matrix.star_dotProduct, starRingEnd_apply, Matrix.mulVec, dotProduct_comm, Matrix.dotProduct_mulVec, Matrix.star_mulVec
-- Module: Mathlib.Analysis.Matrix.PosDef
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 z : n → 𝕜), M *ᵥ z ⬝ᵥ star (x + y) = M *ᵥ z ⬝ᵥ star x + M *ᵥ z ⬝ᵥ star y

Tactic:
simp only [star_add, dotProduct_add, forall_const]

Premises used: StarAddMonoid.star_add, forall_const, dotProduct_add
-- Module: Mathlib.Analysis.Matrix.PosDef
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 x_1 : n → 𝕜
x_2 : 𝕜
rw : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (M *ᵥ x_1 ⬝ᵥ star x)
rw₁ : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = M *ᵥ x_1 ⬝ᵥ HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (star x)
rw₂ : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = M *ᵥ x_1 ⬝ᵥ star x_2 • star x
rw₃ rw₄ : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = M *ᵥ x_1 ⬝ᵥ star (x_2 • x)
⊢ M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (M *ᵥ x_1 ⬝ᵥ star x)

Tactic:
rw [← smul_eq_mul, ← dotProduct_smul, starRingEnd_apply, ← star_smul]

Premises used: StarModule.star_smul, starRingEnd_apply, dotProduct_smul, smul_eq_mul
-- Module: Mathlib.Analysis.Matrix.PosDef
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.PosDef
x : n → 𝕜
hx : M *ᵥ x ⬝ᵥ star x = 0
by_contra! : ∀ (h : x ≠ 0), False
⊢ x = 0

Tactic:
by_contra! h
-- Module: Mathlib.Analysis.Matrix.PosDef
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.PosDef
x : n → 𝕜
hx : M *ᵥ x ⬝ᵥ star x = 0
h : x ≠ 0
⊢ False

Tactic:
simpa [hx, lt_irrefl, dotProduct_comm] using hM.re_dotProduct_pos h

Premises used: lt_irrefl, dotProduct_comm, Matrix.PosDef.re_dotProduct_pos
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
rw : Set.Finite (α := ℝ) ((⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜) ⁻¹' spectrum 𝕜 A)
⊢ (spectrum ℝ A).Finite

Tactic:
rw [← spectrum.preimage_algebraMap 𝕜]

Premises used: spectrum.preimage_algebraMap
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
⊢ Set.Finite (α := ℝ) ((⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜) ⁻¹' spectrum 𝕜 A)

Tactic:
A.finite_spectrum.preimage (FaithfulSMul.algebraMap_injective ℝ 𝕜).injOn

Premises used: Real, Function.Injective.injOn, Matrix.finite_spectrum, FaithfulSMul.algebraMap_injective, Set.Finite.preimage
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
⊢ Set.Finite (α := ℝ) ((⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜) ⁻¹' spectrum 𝕜 A)

Tactic:
exact A.finite_spectrum.preimage (FaithfulSMul.algebraMap_injective ℝ 𝕜).injOn

Premises used: Real, Function.Injective.injOn, Matrix.finite_spectrum, FaithfulSMul.algebraMap_injective, Set.Finite.preimage
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A B : Matrix n n 𝕜
inst_2 : DecidableEq n
⊢ Finite (↑(spectrum ℝ A) : Type)

Tactic:
A.finite_real_spectrum

Premises used: Set.Finite, Matrix.finite_real_spectrum
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
p : ENNReal
⊢ spectrum 𝕜 (A := WithLp p (n → 𝕜) →ₗ[𝕜] WithLp p (n → 𝕜))
      ((toLpLin p p : (a : Matrix n n 𝕜) → WithLp p (n → 𝕜) →ₗ[𝕜] WithLp p (n → 𝕜)) A :
        WithLp p (n → 𝕜) →ₗ[𝕜] WithLp p (n → 𝕜)) =
    spectrum 𝕜 A

Tactic:
AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv (PiLp.basisFun p 𝕜 n)) _

Premises used: Multiset.sum, Multiset.foldr, dotProduct, PiLp.basisFun, AlgEquiv.spectrum_eq, Matrix.toLinAlgEquiv, Matrix.mulVec, Finset.sum
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
⊢ spectrum 𝕜 (A := EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) A :
        EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) =
    spectrum 𝕜 A

Tactic:
spectrum_toLpLin 2

Premises used: Matrix.spectrum_toLpLin, OfNat.ofNat
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ Antitone (α := Fin (Fintype.card n)) hA.eigenvalues₀

Tactic:
LinearMap.IsSymmetric.eigenvalues_antitone ..

Premises used: Matrix.IsHermitian.eigenvalues₀, LinearMap.IsSymmetric.eigenvalues_antitone