awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.PosDef
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.PosDef
⊢ ∀ (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.PosDef
this : ∀ (a b c : R'), a * b * c = c * b * a
⊢ Mᵀ.PosDef

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

Premises used: Matrix.IsHermitian.transpose, And.left, And.intro, Matrix.PosDef
-- 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.PosDef
this : ∀ (a b c : R'), a * b * c = c * b * a
refine :
  ∀ (x : n →₀ R'),
    x ≠ 0 → LT.lt (α := R') 0 (x.sum fun (i : n) (xi : R') ↦ x.sum fun (j : n) (xj : R') ↦ star xi * Mᵀ i j * xj)
⊢ Mᵀ.PosDef

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.PosDef
this : ∀ (a b c : R'), a * b * c = c * b * a
x : n →₀ R'
rw : x ≠ 0 → LT.lt (α := R') 0 (x.sum fun (x' : n) (v' : R') ↦ x.sum fun (x : n) (v : R') ↦ star v * Mᵀ x x' * v')
⊢ x ≠ 0 → LT.lt (α := 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.PosDef
this : ∀ (a b c : R'), a * b * c = c * b * a
x : n →₀ R'
⊢ x ≠ 0 → LT.lt (α := R') 0 (x.sum fun (x' : n) (v' : R') ↦ x.sum fun (x : n) (v : R') ↦ star v * Mᵀ x x' * v')

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

Premises used: star_injective, And.right, Finsupp.sum_mapRange_index
-- 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 : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
⊢ LT.lt (α := 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_pos' (fun _ _ ↦ Finsupp.sum_nonneg ?_) ?_

Premises used: Finsupp.sum_nonneg, Finsupp.sum_pos'
-- 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 : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
refine_1 :
  ∀ x_1 ∈ x.support,
    ∀ i ∈ x.support,
      0 ≤
        HMul.hMul (β := R) (HMul.hMul (α := R) (star ((x : (a : n) → R) x_1) : R) (diagonal d x_1 i))
          ((x : (a : n) → R) i : R)
refine_2 :
  ∃ i ∈ x.support,
    LT.lt (α := R) 0
      (x.sum fun (j : n) (xj : R) ↦ HMul.hMul (α := R) (star ((x : (a : n) → R) i) : R) (diagonal d i j) * xj)
⊢ LT.lt (α := 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_pos' (fun _ _ ↦ Finsupp.sum_nonneg ?_) ?_

Premises used: Finsupp.sum_nonneg, Finsupp.sum_pos'
-- 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 : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
x_1 : n
h_1 : x_1 ∈ x.support
⊢ ∀ i ∈ x.support,
    0 ≤
      HMul.hMul (β := R) (HMul.hMul (α := R) (star ((x : (a : n) → R) x_1) : R) (diagonal d x_1 i))
        ((x : (a : n) → R) i : R)

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

Premises used: apply_ite, LT.lt.le, 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
inst_5 : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
⊢ ∃ (x_1 : n), ¬Eq.{u_3 + 1} (α := R) ((x : (a : n) → R) x_1 : R) (0 : R)

Tactic:
simpa [Finsupp.ext_iff] using hx

Premises used: Finsupp.ext_iff
-- 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 : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
refine_2 :
  ∀ (i : n) (hxi : ¬Eq.{u_3 + 1} (α := R) ((x : (a : n) → R) i : R) (0 : R)),
    ∃ i ∈ x.support,
      LT.lt (α := R) 0
        (x.sum fun (j : n) (xj : R) ↦ HMul.hMul (α := R) (star ((x : (a : n) → R) i) : R) (diagonal d i j) * xj)
⊢ ∃ i ∈ x.support,
    LT.lt (α := R) 0
      (x.sum fun (j : n) (xj : R) ↦ HMul.hMul (α := R) (star ((x : (a : n) → R) i) : R) (diagonal d i j) * xj)

Tactic:
obtain ⟨i, hxi⟩ := by simpa [Finsupp.ext_iff] using hx
-- 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 : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬Eq.{u_3 + 1} (α := R) ((x : (a : n) → R) i : R) (0 : R)
⊢ ∃ i ∈ x.support,
    LT.lt (α := R) 0
      (x.sum fun (j : n) (xj : R) ↦ HMul.hMul (α := R) (star ((x : (a : n) → R) i) : R) (diagonal d i j) * xj)

Tactic:
⟨i, ?_, Finsupp.sum_pos' ?_ ⟨i, ?_, ?_⟩⟩

Premises used: And.intro, Exists.intro, Finsupp.sum_pos'
-- 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 : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬Eq.{u_3 + 1} (α := R) ((x : (a : n) → R) i : R) (0 : R)
refine_2 : i ∈ x.support
refine_2₁ :
  ∀ i_1 ∈ x.support,
    0 ≤
      HMul.hMul (β := R) (HMul.hMul (α := R) (star ((x : (a : n) → R) i) : R) (diagonal d i i_1))
        ((x : (a : n) → R) i_1 : R)
refine_2₂ : i ∈ x.support
refine_2₃ :
  0 <
    HMul.hMul (β := R) (HMul.hMul (α := R) (star ((x : (a : n) → R) i) : R) (diagonal d i i)) ((x : (a : n) → R) i : R)
⊢ ∃ i ∈ x.support,
    LT.lt (α := R) 0
      (x.sum fun (j : n) (xj : R) ↦ HMul.hMul (α := R) (star ((x : (a : n) → R) i) : R) (diagonal d i j) * xj)

Tactic:
refine ⟨i, ?_, Finsupp.sum_pos' ?_ ⟨i, ?_, ?_⟩⟩
-- 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 : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬Eq.{u_3 + 1} (α := R) ((x : (a : n) → R) i : R) (0 : R)
⊢ i ∈ x.support

Tactic:
simp +contextual [diagonal,
      apply_ite, star_left_conjugate_nonneg (h _).le,
      star_left_conjugate_pos (h i), IsRegular.of_ne_zero hxi, Finsupp.mem_support_iff.mpr hxi]

Premises used: Iff.mpr, Finsupp.mem_support_iff, IsRegular.of_ne_zero, star_left_conjugate_pos, apply_ite, LT.lt.le, 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
inst_5 : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬Eq.{u_3 + 1} (α := R) ((x : (a : n) → R) i : R) (0 : R)
⊢ ∀ i_1 ∈ x.support,
    0 ≤
      HMul.hMul (β := R) (HMul.hMul (α := R) (star ((x : (a : n) → R) i) : R) (diagonal d i i_1))
        ((x : (a : n) → R) i_1 : R)

Tactic:
simp +contextual [diagonal,
      apply_ite, star_left_conjugate_nonneg (h _).le,
      star_left_conjugate_pos (h i), IsRegular.of_ne_zero hxi, Finsupp.mem_support_iff.mpr hxi]

Premises used: Iff.mpr, Finsupp.mem_support_iff, IsRegular.of_ne_zero, star_left_conjugate_pos, apply_ite, LT.lt.le, 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
inst_5 : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬Eq.{u_3 + 1} (α := R) ((x : (a : n) → R) i : R) (0 : R)
⊢ 0 <
    HMul.hMul (β := R) (HMul.hMul (α := R) (star ((x : (a : n) → R) i) : R) (diagonal d i i)) ((x : (a : n) → R) i : R)

Tactic:
simp +contextual [diagonal,
      apply_ite, star_left_conjugate_nonneg (h _).le,
      star_left_conjugate_pos (h i), IsRegular.of_ne_zero hxi, Finsupp.mem_support_iff.mpr hxi]

Premises used: Iff.mpr, Finsupp.mem_support_iff, IsRegular.of_ne_zero, star_left_conjugate_pos, apply_ite, LT.lt.le, 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
inst_5 : NoZeroDivisors R
inst_6 : Nontrivial R
d : n → R
h : (diagonal d).PosDef
i : n
⊢ 0 < d i

Tactic:
simpa using h.2 (x := .single i 1)

Premises used: 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
h : Subsingleton R
M : Matrix n n R
⊢ M.PosDef

Tactic:
⟨.of_subsingleton, fun _ hx ↦ (hx <| Subsingleton.elim ..).elim⟩

Premises used: False.elim, And.intro, Matrix.IsHermitian.of_subsingleton, Matrix.PosDef, Subsingleton.elim, OfNat.ofNat
-- 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 : NoZeroDivisors R
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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 : NoZeroDivisors R
h : Nontrivial R
⊢ PosDef.{u_2, u_3} (n := n) (R := R) 1

Tactic:
.diagonal fun i ↦ zero_lt_one' R

Premises used: zero_lt_one', Matrix.PosDef.diagonal
-- 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 : NoZeroDivisors R
h : Nontrivial R
⊢ PosDef.{u_2, u_3} (n := n) (R := R) 1

Tactic:
exact .diagonal fun i ↦ zero_lt_one' R
-- 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 : NoZeroDivisors R
d : ℕ
hd : d ≠ 0
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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 : NoZeroDivisors R
d : ℕ
hd : d ≠ 0
h : Nontrivial R
x : n
⊢ LT.lt.{u_3} (α := R) 0 (↑d : R)

Tactic:
simpa [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- 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 : NoZeroDivisors R
d : ℕ
hd : d ≠ 0
h : Nontrivial R
⊢ PosDef.{u_2, u_3} (n := n) (R := R) (↑d : Matrix n n R)

Tactic:
exact .diagonal fun _ ↦ by simpa [pos_iff_ne_zero]
-- 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 : NoZeroDivisors R
inst_6 : Nonempty n
inst_7 : Nontrivial R
d : ℕ
⊢ (∀ (i : n), LT.lt.{u_3} (α := R) 0 (↑d : R)) ↔ 0 < d

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
inst_5 : NoZeroDivisors R
d : ℕ
inst_6 : d.AtLeastTwo
⊢ PosDef.{u_2, u_3} (n := n) (R := R) (OfNat.ofNat d)

Tactic:
.natCast d (NeZero.ne _)

Premises used: Matrix.PosDef.natCast, NeZero.ne
-- 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 : NoZeroDivisors R
d : ℤ
hd : 0 < d
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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 : NoZeroDivisors R
d : ℤ
hd : 0 < d
h : Nontrivial R
x : n
⊢ LT.lt.{u_3} (α := R) 0 (↑d : R)

Tactic:
simpa [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- 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 : NoZeroDivisors R
d : ℤ
hd : 0 < d
h : Nontrivial R
⊢ PosDef.{u_2, u_3} (n := n) (R := R) (↑d : Matrix n n R)

Tactic:
exact .diagonal fun _ ↦ by simpa [pos_iff_ne_zero]
-- 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 : NoZeroDivisors R
inst_6 : Nonempty n
inst_7 : Nontrivial R
d : ℤ
⊢ (∀ (i : n), LT.lt.{u_3} (α := R) 0 (↑d : R)) ↔ 0 < d

Tactic:
simp
-- 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.PosDef
hB : B.PosSemidef
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 * (A + B) i j * xj)

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

Premises used: add_mul, And.right, mul_add, add_pos_of_pos_of_nonneg
-- 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.PosDef
⊢ (A + B).PosDef

Tactic:
add_comm A B ▸ hB.add_posSemidef hA

Premises used: Eq.rec, add_comm, Matrix.PosDef.add_posSemidef, 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.PosDef
hB : B.PosDef
⊢ (A + B).PosDef

Tactic:
hA.add_posSemidef hB.posSemidef

Premises used: Matrix.PosDef.add_posSemidef, Matrix.PosDef.posSemidef
-- 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
ι : Type u_5
inst_3 : AddLeftMono R
A : ι → Matrix m m R
hs : Finset.Nonempty.{u_5} (α := ι) ∅
hA : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (A i).PosDef
⊢ PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ ∅, A i)

Tactic:
simp at hs
-- 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
ι : Type u_5
inst_3 : AddLeftMono R
A : ι → Matrix m m R
i : ι
hi : Finset ι
hins : i ∉ hi
H : ∀ (hs : hi.Nonempty) (hA : ∀ i ∈ hi, (A i).PosDef), PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ hi, A i)
hs : (Insert.insert i hi).Nonempty
hA : ∀ i_1 ∈ Insert.insert i hi, (A i_1).PosDef
insert : (A i + ∑ x ∈ hi, A x).PosDef
⊢ PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ Insert.insert i hi, A i)

Tactic:
rw [Finset.sum_insert hins]

Premises used: Finset.sum_insert
-- 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
ι : Type u_5
inst_3 : AddLeftMono R
A : ι → Matrix m m R
i : ι
hi : Finset ι
hins : i ∉ hi
H : ∀ (hs : hi.Nonempty) (hA : ∀ i ∈ hi, (A i).PosDef), PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ hi, A i)
hs : (insert i hi).Nonempty
hA : ∀ i_1 ∈ insert i hi, (A i_1).PosDef
pos : ∀ (h : ¬hi.Nonempty), (A i + ∑ x ∈ hi, A x).PosDef
neg : ∀ (h : ¬¬hi.Nonempty), (A i + ∑ x ∈ hi, A x).PosDef
⊢ (A i + ∑ x ∈ hi, A x).PosDef

Tactic:
by_cases h : ¬ hi.Nonempty

Premises used: Finset.Nonempty
-- 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
ι : Type u_5
inst_3 : AddLeftMono R
A : ι → Matrix m m R
i : ι
hi : Finset ι
hins : i ∉ hi
H : ∀ (hs : hi.Nonempty) (hA : ∀ i ∈ hi, (A i).PosDef), PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ hi, A i)
hs : (insert i hi).Nonempty
hA : ∀ i_1 ∈ insert i hi, (A i_1).PosDef
h : ¬hi.Nonempty
⊢ (A i + ∑ x ∈ hi, A x).PosDef

Tactic:
simp_all
-- 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
ι : Type u_5
inst_3 : AddLeftMono R
A : ι → Matrix m m R
i : ι
hi : Finset ι
hins : i ∉ hi
H : ∀ (hs : hi.Nonempty) (hA : ∀ i ∈ hi, (A i).PosDef), PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ hi, A i)
hs : (insert i hi).Nonempty
hA : ∀ i_1 ∈ insert i hi, (A i_1).PosDef
h : ¬¬hi.Nonempty
⊢ (A i + ∑ x ∈ hi, A x).PosDef

Tactic:
PosDef.add (hA _ <| Finset.mem_insert_self i hi) <|
          H (not_not.mp h) fun _ _hi => hA _ (Finset.mem_insert_of_mem _hi)

Premises used: Finset.mem_insert_self, Classical.not_not, Matrix.PosDef.add, Finset.mem_insert_of_mem, Iff.mp
-- 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
ι : Type u_5
inst_3 : AddLeftMono R
A : ι → Matrix m m R
i : ι
hi : Finset ι
hins : i ∉ hi
H : ∀ (hs : hi.Nonempty) (hA : ∀ i ∈ hi, (A i).PosDef), PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ hi, A i)
hs : (insert i hi).Nonempty
hA : ∀ i_1 ∈ insert i hi, (A i_1).PosDef
h : ¬¬hi.Nonempty
⊢ (A i + ∑ x ∈ hi, A x).PosDef

Tactic:
exact PosDef.add (hA _ <| Finset.mem_insert_self i hi) <|
          H (not_not.mp h) fun _ _hi => hA _ (Finset.mem_insert_of_mem _hi)

Premises used: Finset.mem_insert_self, Classical.not_not, Matrix.PosDef.add, Finset.mem_insert_of_mem, Iff.mp
-- 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
ι : Type u_5
inst_3 : AddLeftMono R
A : ι → Matrix m m R
s : Finset ι
hs : s.Nonempty
hA : ∀ i ∈ s, (A i).PosDef
empty :
  ∀ (hs : Finset.Nonempty.{u_5} (α := ι) ∅) (hA : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (A i).PosDef),
    PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ ∅, A i)
insert :
  ∀ (i : ι) (hi : Finset ι) (hins : i ∉ hi)
    (H : ∀ (hs : hi.Nonempty) (hA : ∀ i ∈ hi, (A i).PosDef), PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ hi, A i))
    (hs : (Insert.insert i hi).Nonempty) (hA : ∀ i_1 ∈ Insert.insert i hi, (A i_1).PosDef),
    PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ Insert.insert i hi, A i)
⊢ PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ s, A i)

Tactic:
induction s using Finset.induction_on with
  | empty => simp at hs
  | insert i hi hins H =>
      rw [Finset.sum_insert hins]
      by_cases h : ¬ hi.Nonempty
      · simp_all
      · exact PosDef.add (hA _ <| Finset.mem_insert_self i hi) <|
          H (not_not.mp h) fun _ _hi => hA _ (Finset.mem_insert_of_mem _hi)

Premises used: Insert.insert
-- 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
ι : Type u_5
inst_3 : AddLeftMono R
A : ι → Matrix m m R
s : Finset ι
hs : s.Nonempty
hA : ∀ i ∈ s, (A i).PosDef
empty :
  ∀ (hs : Finset.Nonempty.{u_5} (α := ι) ∅) (hA : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (A i).PosDef),
    PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ ∅, A i)
insert :
  ∀ (i : ι) (hi : Finset ι) (hins : i ∉ hi)
    (H : ∀ (hs : hi.Nonempty) (hA : ∀ i ∈ hi, (A i).PosDef), PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ hi, A i))
    (hs : (Insert.insert i hi).Nonempty) (hA : ∀ i_1 ∈ Insert.insert i hi, (A i_1).PosDef),
    PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ Insert.insert i hi, A i)
⊢ PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ s, A i)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp at hs
  | insert i hi hins H =>
      rw [Finset.sum_insert hins]
      by_cases h : ¬ hi.Nonempty
      · simp_all
      · exact PosDef.add (hA _ <| Finset.mem_insert_self i hi) <|
          H (not_not.mp h) fun _ _hi => hA _ (Finset.mem_insert_of_mem _hi)

Premises used: Insert.insert
-- 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 : PosSMulStrictMono α R
x : Matrix n n R
hx : x.PosDef
a : α
ha : 0 < a
⊢ (a • x).PosDef

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

Premises used: LT.lt.le, IsSelfAdjoint.of_nonneg, And.left, And.intro, Matrix.PosDef, 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 : PosSMulStrictMono α R
x : Matrix n n R
hx : x.PosDef
a : α
ha : 0 < a
refine :
  ∀ (y : n →₀ R) (hy : y ≠ 0),
    LT.lt (α := 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).PosDef

Tactic:
refine ⟨IsSelfAdjoint.smul (IsSelfAdjoint.of_nonneg ha.le) hx.1, fun y hy => ?_⟩
-- 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 : PosSMulStrictMono α R
x : Matrix n n R
hx : x.PosDef
a : α
ha : 0 < a
y : n →₀ R
hy : y ≠ 0
⊢ LT.lt (α := 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 [← Finsupp.smul_sum] using smul_pos ha (hx.2 hy)

Premises used: And.right, smul_pos, 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
M : Matrix n n R
hM : M.PosDef
⊢ Mᴴ.PosDef

Tactic:
hM.1.symm ▸ hM

Premises used: Eq.rec, And.left, Eq.symm
-- 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 : Nontrivial R
A : Matrix n n R
hA : A.PosDef
i : n
⊢ 0 < A i i

Tactic:
simpa [trace] using hA.2 (x := Finsupp.single i 1)

Premises used: Matrix.trace, 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
inst_3 : Nontrivial R
A : Matrix n n R
hA : A.PosDef
i : n
⊢ 0 < A i i

Tactic:
classical simpa [trace] using hA.2 (x := Finsupp.single i 1)

Premises used: Matrix.trace, 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
inst_3 : Fintype n
M : Matrix n n R
⊢ M.PosSemidef ↔ M.IsHermitian ∧ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ M *ᵥ x

Tactic:
simp [PosSemidef, ← Finsupp.equivFunOnFinite.forall_congr_right, dotProduct, mulVec,
    Finsupp.sum_fintype, Finset.mul_sum, mul_assoc]

Premises used: Finset.mul_sum, dotProduct, Finsupp.sum_fintype, mul_assoc, Finsupp.equivFunOnFinite, Matrix.PosSemidef, Equiv.forall_congr_right, Matrix.mulVec