awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h_1 : Nontrivial α
h :
  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (Matrix.map (α := α) 1 (⇑C : (a : α) → α[X])) +
          A.map (⇑C : (a : α) → α[X])).det.natDegree =
    Fintype.card n
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.natDegree =
    Fintype.card n

Tactic:
simp only [map_one, Matrix.map_one, C_eq_zero] at h

Premises used: Polynomial.C_eq_zero, Matrix.map_one, map_one
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h_1 : Nontrivial α
h :
  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.natDegree =
    Fintype.card n
inr inr₁ :
  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
      (Fintype.card n) =
    (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
      (Fintype.card n)
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
      (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.natDegree =
    (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
      (Fintype.card n)

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h_1 : Nontrivial α
h :
  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (Matrix.map (α := α) 1 (⇑C : (a : α) → α[X])) +
          A.map (⇑C : (a : α) → α[X])).det.natDegree <
    Fintype.card n
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (Matrix.map (α := α) 1 (⇑C : (a : α) → α[X])) +
            A.map (⇑C : (a : α) → α[X])).det.coeff
      (Fintype.card n) =
    0

Tactic:
have H := coeff_eq_zero_of_natDegree_lt h
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h_1 : Nontrivial α
h :
  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (Matrix.map (α := α) 1 (⇑C : (a : α) → α[X])) +
          A.map (⇑C : (a : α) → α[X])).det.natDegree <
    Fintype.card n
H :
  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (Matrix.map (α := α) 1 (⇑C : (a : α) → α[X])) +
            A.map (⇑C : (a : α) → α[X])).det.coeff
      (Fintype.card n) =
    0
⊢ Eq.{u_2 + 1} (α := α) (det.{u_2, u_1} (n := n) 1) 0

Tactic:
rw [coeff_det_X_add_C_card] at H

Premises used: Polynomial.coeff_det_X_add_C_card
-- Module: Mathlib.LinearAlgebra.Matrix.Polynomial
Goal:
n : Type u_1
α : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h_1 : Nontrivial α
h :
  (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X (Matrix.map (α := α) 1 (⇑C : (a : α) → α[X])) +
          A.map (⇑C : (a : α) → α[X])).det.natDegree <
    Fintype.card n
H : Eq.{u_2 + 1} (α := α) (det.{u_2, u_1} (n := n) 1) 0
⊢ (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
      (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.natDegree =
    (HSMul.hSMul (α := α[X]) (β := Matrix.{u_1, u_1, u_2} n n α[X]) X 1 + A.map (⇑C : (a : α) → α[X])).det.coeff
      (Fintype.card n)

Tactic:
simp at H
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
d : n → R
h : 0 ≤ d
x : n →₀ R
⊢ LE.le (α := R) 0 (x.sum fun (i : n) (xi : R) ↦ x.sum fun (j : n) (xj : R) ↦ star xi * diagonal d i j * xj)

Tactic:
Finsupp.sum_nonneg fun i _ ↦ Finsupp.sum_nonneg fun j _ ↦ ?_

Premises used: Finsupp.sum_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
d : n → R
h : 0 ≤ d
x : n →₀ R
refine :
  ∀ i ∈ x.support,
    ∀ j ∈ x.support,
      0 ≤
        HMul.hMul (β := R) (HMul.hMul (α := R) (star ((x : (a : n) → R) i) : R) (diagonal d i j))
          ((x : (a : n) → R) j : R)
⊢ LE.le (α := R) 0 (x.sum fun (i : n) (xi : R) ↦ x.sum fun (j : n) (xj : R) ↦ star xi * diagonal d i j * xj)

Tactic:
refine Finsupp.sum_nonneg fun i _ ↦ Finsupp.sum_nonneg fun j _ ↦ ?_

Premises used: Finsupp.sum_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
d : n → R
h : 0 ≤ d
x : n →₀ R
i : n
h_1 : i ∈ x.support
j : n
h_2 : j ∈ x.support
⊢ 0 ≤
    HMul.hMul (β := R) (HMul.hMul (α := R) (star ((x : (a : n) → R) i) : R) (diagonal d i j)) ((x : (a : n) → R) j : R)

Tactic:
simp +contextual [diagonal, apply_ite, star_left_conjugate_nonneg (h _)]

Premises used: apply_ite, Matrix.diagonal, star_left_conjugate_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
d : n → R
h : (diagonal d).PosSemidef
i : n
left : (diagonal d).IsHermitian
hP :
  ∀ (x : n →₀ R),
    LE.le (α := R) 0 (x.sum fun (i : n) (xi : R) ↦ x.sum fun (j : n) (xj : R) ↦ star xi * diagonal d i j * xj)
⊢ 0 ≤ d i

Tactic:
simpa using hP (.single i 1)

Premises used: OfNat.ofNat, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosSemidef
⊢ M.IsHermitian

Tactic:
hM.1

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosSemidef
e : m → n
⊢ (M.submatrix e e).PosSemidef

Tactic:
⟨hM.1.submatrix _, fun x ↦ ?_⟩

Premises used: Matrix.PosSemidef, And.left, And.intro, Matrix.IsHermitian.submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosSemidef
e : m → n
refine :
  ∀ (x : m →₀ R),
    LE.le (α := R) 0 (x.sum fun (i : m) (xi : R) ↦ x.sum fun (j : m) (xj : R) ↦ star xi * M.submatrix e e i j * xj)
⊢ (M.submatrix e e).PosSemidef

Tactic:
refine ⟨hM.1.submatrix _, fun x ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosSemidef
e : m → n
x : m →₀ R
⊢ LE.le (α := R) 0 (x.sum fun (i : m) (xi : R) ↦ x.sum fun (j : m) (xj : R) ↦ star xi * M.submatrix e e i j * xj)

Tactic:
simpa [Finsupp.sum_mapDomain_index, add_mul, mul_add] using hM.2 <| x.mapDomain e

Premises used: add_mul, Finsupp.mapDomain, Finsupp.sum_mapDomain_index, And.right, mul_add
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
M : Matrix n n R'
hM : M.PosSemidef
a b c : R'
⊢ a * b * c = c * b * a

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
M : Matrix n n R'
hM : M.PosSemidef
⊢ ∀ (a b c : R'), a * b * c = c * b * a

Tactic:
have (a b c : R') : a * b * c = c * b * a := by ring
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
M : Matrix n n R'
hM : M.PosSemidef
this : ∀ (a b c : R'), a * b * c = c * b * a
⊢ Mᵀ.PosSemidef

Tactic:
⟨hM.1.transpose, fun x => ?_⟩

Premises used: Matrix.IsHermitian.transpose, Matrix.PosSemidef, And.left, And.intro
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
M : Matrix n n R'
hM : M.PosSemidef
this : ∀ (a b c : R'), a * b * c = c * b * a
refine :
  ∀ (x : n →₀ R'), LE.le (α := R') 0 (x.sum fun (i : n) (xi : R') ↦ x.sum fun (j : n) (xj : R') ↦ star xi * Mᵀ i j * xj)
⊢ Mᵀ.PosSemidef

Tactic:
refine ⟨hM.1.transpose, fun x => ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
M : Matrix n n R'
hM : M.PosSemidef
this : ∀ (a b c : R'), a * b * c = c * b * a
x : n →₀ R'
rw : LE.le (α := R') 0 (x.sum fun (x' : n) (v' : R') ↦ x.sum fun (x : n) (v : R') ↦ star v * Mᵀ x x' * v')
⊢ LE.le (α := R') 0 (x.sum fun (i : n) (xi : R') ↦ x.sum fun (j : n) (xj : R') ↦ star xi * Mᵀ i j * xj)

Tactic:
rw [Finsupp.sum_comm]

Premises used: Finsupp.sum_comm
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
M : Matrix n n R'
hM : M.PosSemidef
this : ∀ (a b c : R'), a * b * c = c * b * a
x : n →₀ R'
⊢ LE.le (α := R') 0 (x.sum fun (x' : n) (v' : R') ↦ x.sum fun (x : n) (v : R') ↦ star v * Mᵀ x x' * v')

Tactic:
simpa [Finsupp.sum_mapRange_index, this] using hM.2 (Finsupp.mapRange star (star_zero R') x)

Premises used: And.right, star_zero, Finsupp.sum_mapRange_index, Finsupp.mapRange, Star.star
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
M : Matrix n n R'
⊢ Mᵀ.PosSemidef ↔ M.PosSemidef

Tactic:
⟨.transpose, .transpose⟩

Premises used: Matrix.PosSemidef.transpose, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosSemidef
⊢ Mᴴ.PosSemidef

Tactic:
hM.1.symm ▸ hM

Premises used: Eq.rec, And.left, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : AddLeftMono R
A B : Matrix m m R
hA : A.PosSemidef
hB : B.PosSemidef
x : m →₀ R
⊢ LE.le (α := R) 0 (x.sum fun (i : m) (xi : R) ↦ x.sum fun (j : m) (xj : R) ↦ star xi * (A + B) i j * xj)

Tactic:
simpa [mul_add, add_mul] using add_nonneg (hA.2 x) (hB.2 x)

Premises used: add_mul, add_nonneg, And.right, mul_add
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
α : Type u_5
inst_3 : CommSemiring α
inst_4 : PartialOrder α
inst_5 : StarRing α
inst_6 : StarOrderedRing α
inst_7 : Algebra α R
inst_8 : StarModule α R
inst_9 : PosSMulMono α R
x : Matrix n n R
hx : x.PosSemidef
a : α
ha : 0 ≤ a
⊢ (a • x).PosSemidef

Tactic:
⟨IsSelfAdjoint.smul (.of_nonneg ha) hx.1, fun y => ?_⟩

Premises used: IsSelfAdjoint.of_nonneg, Matrix.PosSemidef, And.left, And.intro, IsSelfAdjoint.smul
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
α : Type u_5
inst_3 : CommSemiring α
inst_4 : PartialOrder α
inst_5 : StarRing α
inst_6 : StarOrderedRing α
inst_7 : Algebra α R
inst_8 : StarModule α R
inst_9 : PosSMulMono α R
x : Matrix n n R
hx : x.PosSemidef
a : α
ha : 0 ≤ a
refine :
  ∀ (y : n →₀ R),
    LE.le (α := R) 0 (y.sum fun (i : n) (xi : R) ↦ y.sum fun (j : n) (xj : R) ↦ star xi * (a • x) i j * xj)
⊢ (a • x).PosSemidef

Tactic:
refine ⟨IsSelfAdjoint.smul (.of_nonneg ha) hx.1, fun y => ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
α : Type u_5
inst_3 : CommSemiring α
inst_4 : PartialOrder α
inst_5 : StarRing α
inst_6 : StarOrderedRing α
inst_7 : Algebra α R
inst_8 : StarModule α R
inst_9 : PosSMulMono α R
x : Matrix n n R
hx : x.PosSemidef
a : α
ha : 0 ≤ a
y : n →₀ R
⊢ LE.le (α := R) 0 (y.sum fun (i : n) (xi : R) ↦ y.sum fun (j : n) (xj : R) ↦ star xi * (a • x) i j * xj)

Tactic:
simpa [mul_smul_comm, smul_mul_assoc, ← Finsupp.smul_sum] using smul_nonneg ha (hx.2 _)

Premises used: smul_nonneg, smul_mul_assoc, And.right, mul_smul_comm, Finsupp.smul_sum
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
⊢ ∀ (x : n →₀ R), LE.le (α := R) 0 (x.sum fun (i : n) (xi : R) ↦ x.sum fun (j : n) (xj : R) ↦ star xi * 0 i j * xj)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
x : n →₀ R
i : n
h : i ∈ x.support
j : n
h_1 : j ∈ x.support
inl :
  i ∈ x.support →
    0 ≤
      HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) (1 i i : R))
        ((x : (a : n) → R) i : R)
inr :
  ∀ (hij : i ≠ j),
    0 ≤
      HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) (1 i j : R))
        ((x : (a : n) → R) j : R)
⊢ 0 ≤
    HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) (1 i j : R))
      ((x : (a : n) → R) j : R)

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
x : n →₀ R
i : n
h h_1 : i ∈ x.support
⊢ 0 ≤
    HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) (1 i i : R))
      ((x : (a : n) → R) i : R)

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
x : n →₀ R
i : n
h : i ∈ x.support
j : n
h_1 : j ∈ x.support
hij : i ≠ j
⊢ 0 ≤
    HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) (1 i j : R))
      ((x : (a : n) → R) j : R)

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
d : ℕ
x : n →₀ R
i : n
h : i ∈ x.support
j : n
h_1 : j ∈ x.support
inl :
  i ∈ x.support →
    0 ≤
      HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) ((↑d : Matrix n n R) i i : R))
        ((x : (a : n) → R) i : R)
inr :
  ∀ (hij : i ≠ j),
    0 ≤
      HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) ((↑d : Matrix n n R) i j : R))
        ((x : (a : n) → R) j : R)
⊢ 0 ≤
    HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) ((↑d : Matrix n n R) i j : R))
      ((x : (a : n) → R) j : R)

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
d : ℕ
x : n →₀ R
i : n
h h_1 : i ∈ x.support
⊢ 0 ≤
    HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) ((↑d : Matrix n n R) i i : R))
      ((x : (a : n) → R) i : R)

Tactic:
simp [← diagonal_natCast', star_left_conjugate_nonneg, *]

Premises used: Matrix.diagonal_natCast', star_left_conjugate_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
d : ℕ
x : n →₀ R
i : n
h : i ∈ x.support
j : n
h_1 : j ∈ x.support
hij : i ≠ j
⊢ 0 ≤
    HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) ((↑d : Matrix n n R) i j : R))
      ((x : (a : n) → R) j : R)

Tactic:
simp [← diagonal_natCast', star_left_conjugate_nonneg, *]

Premises used: Matrix.diagonal_natCast', star_left_conjugate_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
d : ℕ
inst_5 : d.AtLeastTwo
⊢ PosSemidef.{u_2, u_3} (n := n) (R := R) (OfNat.ofNat d)

Tactic:
.natCast d

Premises used: Matrix.PosSemidef.natCast
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
d : ℤ
hd : 0 ≤ d
x : n →₀ R
i : n
h : i ∈ x.support
j : n
h_1 : j ∈ x.support
inl :
  i ∈ x.support →
    0 ≤
      HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) ((↑d : Matrix n n R) i i : R))
        ((x : (a : n) → R) i : R)
inr :
  ∀ (hij : i ≠ j),
    0 ≤
      HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) ((↑d : Matrix n n R) i j : R))
        ((x : (a : n) → R) j : R)
⊢ 0 ≤
    HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) ((↑d : Matrix n n R) i j : R))
      ((x : (a : n) → R) j : R)

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
d : ℤ
hd : 0 ≤ d
x : n →₀ R
i : n
h h_1 : i ∈ x.support
⊢ 0 ≤
    HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) ((↑d : Matrix n n R) i i : R))
      ((x : (a : n) → R) i : R)

Tactic:
simp [← diagonal_intCast', star_left_conjugate_nonneg, *]

Premises used: Matrix.diagonal_intCast', star_left_conjugate_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
d : ℤ
hd : 0 ≤ d
x : n →₀ R
i : n
h : i ∈ x.support
j : n
h_1 : j ∈ x.support
hij : i ≠ j
⊢ 0 ≤
    HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (star ((x : (a : n) → R) i) : R) ((↑d : Matrix n n R) i j : R))
      ((x : (a : n) → R) j : R)

Tactic:
simp [← diagonal_intCast', star_left_conjugate_nonneg, *]

Premises used: Matrix.diagonal_intCast', star_left_conjugate_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : DecidableEq n
inst_5 : Nonempty n
inst_6 : Nontrivial R
d : ℤ
⊢ PosSemidef.{u_2, u_3} (n := n) (R := R) (↑d : Matrix n n R) ↔ 0 ≤ d

Tactic:
simp [← diagonal_intCast']

Premises used: Matrix.diagonal_intCast'
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
A : Matrix n n R
hA : A.PosSemidef
i : n
⊢ 0 ≤ A i i

Tactic:
simpa using hA.2 <| .single i 1

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
e : m ≃ n
h : PosSemidef.{u_1, u_3} (n := m) (M.submatrix (⇑e : (a : m) → n) (⇑e : (a : m) → n))
⊢ M.PosSemidef

Tactic:
simpa using h.submatrix e.symm

Premises used: Matrix.PosSemidef.submatrix, Equiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
ι : Type u_5
inst_3 : AddLeftMono R
x : ι → Matrix n n R
s : Finset ι
h : ∀ i ∈ s, (x i).PosSemidef
⊢ PosSemidef.{u_2, u_3} (n := n) (R := R) (∑ i ∈ s, x i)

Tactic:
⟨isSelfAdjoint_sum s fun _ hi => h _ hi |>.1, fun y => ?_⟩

Premises used: isSelfAdjoint_sum, Matrix.PosSemidef, And.left, And.intro
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
ι : Type u_5
inst_3 : AddLeftMono R
x : ι → Matrix n n R
s : Finset ι
h : ∀ i ∈ s, (x i).PosSemidef
refine :
  ∀ (y : n →₀ R),
    LE.le (α := R) 0 (y.sum fun (i : n) (xi : R) ↦ y.sum fun (j : n) (xj : R) ↦ star xi * (∑ i ∈ s, x i) i j * xj)
⊢ PosSemidef.{u_2, u_3} (n := n) (R := R) (∑ i ∈ s, x i)

Tactic:
refine ⟨isSelfAdjoint_sum s fun _ hi => h _ hi |>.1, fun y => ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
ι : Type u_5
inst_3 : AddLeftMono R
x : ι → Matrix n n R
s : Finset ι
h : ∀ i ∈ s, (x i).PosSemidef
y : n →₀ R
⊢ LE.le (α := R) 0 (y.sum fun (i : n) (xi : R) ↦ y.sum fun (j : n) (xj : R) ↦ star xi * (∑ i ∈ s, x i) i j * xj)

Tactic:
simp [sum_apply, Finset.mul_sum, Finset.sum_mul, Finsupp.sum_finsetSum_comm,
    Finset.sum_nonneg fun _ hi => (h _ hi).2 _]

Premises used: Finset.mul_sum, Finsupp.sum_finsetSum_comm, Matrix.sum_apply, Finset.sum_nonneg, And.right, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosDef
⊢ M.IsHermitian

Tactic:
hM.1

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n →₀ R
inl :
  LE.le.{u_3} (α := R) 0
    (Finsupp.sum 0 fun (i : n) (xi : R) ↦ Finsupp.sum 0 fun (j : n) (xj : R) ↦ star xi * M i j * xj)
inr : ∀ (hx : x ≠ 0), LE.le (α := R) 0 (x.sum fun (i : n) (xi : R) ↦ x.sum fun (j : n) (xj : R) ↦ star xi * M i j * xj)
⊢ LE.le (α := R) 0 (x.sum fun (i : n) (xi : R) ↦ x.sum fun (j : n) (xj : R) ↦ star xi * M i j * xj)

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosDef
⊢ LE.le.{u_3} (α := R) 0
    (Finsupp.sum 0 fun (i : n) (xi : R) ↦ Finsupp.sum 0 fun (j : n) (xj : R) ↦ star xi * M i j * xj)

Tactic:
simp [le_of_lt, hM.2, *]

Premises used: le_of_lt, And.right
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n →₀ R
hx : x ≠ 0
⊢ LE.le (α := R) 0 (x.sum fun (i : n) (xi : R) ↦ x.sum fun (j : n) (xj : R) ↦ star xi * M i j * xj)

Tactic:
simp [le_of_lt, hM.2, *]

Premises used: le_of_lt, And.right
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosDef
e : m → n
he : Function.Injective e
⊢ (M.submatrix e e).PosDef

Tactic:
⟨hM.1.submatrix _, fun x hx ↦ ?_⟩

Premises used: And.left, And.intro, Matrix.PosDef, Matrix.IsHermitian.submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosDef
e : m → n
he : Function.Injective e
refine :
  ∀ (x : m →₀ R) (hx : x ≠ 0),
    LT.lt (α := R) 0 (x.sum fun (i : m) (xi : R) ↦ x.sum fun (j : m) (xj : R) ↦ star xi * M.submatrix e e i j * xj)
⊢ (M.submatrix e e).PosDef

Tactic:
refine ⟨hM.1.submatrix _, fun x hx ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.PosDef
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
M : Matrix n n R
hM : M.PosDef
e : m → n
he : Function.Injective e
x : m →₀ R
hx : x ≠ 0
⊢ LT.lt (α := R) 0 (x.sum fun (i : m) (xi : R) ↦ x.sum fun (j : m) (xj : R) ↦ star xi * M.submatrix e e i j * xj)

Tactic:
simpa [Finsupp.sum_mapDomain_index, add_mul, mul_add] using
    hM.2 <| Finsupp.mapDomain_injective he |>.ne_iff' Finsupp.mapDomain_zero |>.2 hx

Premises used: Iff.mpr, add_mul, Finsupp.sum_mapDomain_index, Finsupp.mapDomain_zero, And.right, mul_add, Function.Injective.ne_iff', Finsupp.mapDomain_injective