awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
have 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)
Tactic: refine ⟨IsSelfAdjoint.smul (.of_nonneg ha) hx.1, fun y => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ 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)
have 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)
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j, h_1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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)
⊢ 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)
have 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)
Tactic: obtain rfl | hij := eq_or_ne i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ 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)
have 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)
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j, h_1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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)
⊢ 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)
have 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)
Tactic: obtain rfl | hij := eq_or_ne i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ 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)
have 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)
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j, h_1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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)
⊢ 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)
have 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)
Tactic: obtain rfl | hij := eq_or_ne i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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)
have 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)
Tactic: refine ⟨isSelfAdjoint_sum s fun _ hi => h _ hi |>.1, fun y => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ LE.le (α := R) 0 (x.sum fun (i : n) (xi : R) ↦ x.sum fun (j : n) (xj : R) ↦ star xi * M i j * xj)
have 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)
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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)
⊢ LE.le (α := R) 0 (x.sum fun (i : n) (xi : R) ↦ x.sum fun (j : n) (xj : R) ↦ star xi * M i j * xj)
have 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)
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
have 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)
Tactic: refine ⟨hM.1.submatrix _, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
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
⊢ Mᵀ.PosDef
have this : ∀ (a b c : R'), a * b * c = c * b * a
Tactic: have (a b c : R') : a * b * c = c * b * a := by ring
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
have 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)
Tactic: refine ⟨hM.1.transpose, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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 (i : n) (xi : R') ↦ x.sum fun (j : n) (xj : R') ↦ star xi * Mᵀ i j * xj)
have 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')
Tactic: rw [Finsupp.sum_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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)
have 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)
Tactic: refine Finsupp.sum_pos' (fun _ _ ↦ Finsupp.sum_nonneg ?_) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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)
⊢ 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)
have 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)
Tactic: refine Finsupp.sum_pos' (fun _ _ ↦ Finsupp.sum_nonneg ?_) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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 ∈ 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)
have 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)
Tactic: obtain ⟨i, hxi⟩ := by simpa [Finsupp.ext_iff] using hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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)
have refine_2 : i ∈ x.support
Tactic: refine ⟨i, ?_, Finsupp.sum_pos' ?_ ⟨i, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ ∃ 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)
have 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)
Tactic: refine ⟨i, ?_, Finsupp.sum_pos' ?_ ⟨i, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ ∃ 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)
have 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)
Tactic: refine ⟨i, ?_, Finsupp.sum_pos' ?_ ⟨i, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
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
⊢ PosDef.{u_2, u_3} (n := n) (R := R) 1
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
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
⊢ PosDef.{u_2, u_3} (n := n) (R := R) (↑d : Matrix n n R)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
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
⊢ PosDef.{u_2, u_3} (n := n) (R := R) (↑d : Matrix n n R)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ insert i hi, A i)
have insert : (A i + ∑ x ∈ hi, A x).PosDef
Tactic: rw [Finset.sum_insert hins]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ (A i + ∑ x ∈ hi, A x).PosDef
have pos : ∀ (h : ¬hi.Nonempty), (A i + ∑ x ∈ hi, A x).PosDef
Tactic: by_cases h : ¬ hi.Nonempty
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ (A i + ∑ x ∈ hi, A x).PosDef
have neg : ∀ (h : ¬¬hi.Nonempty), (A i + ∑ x ∈ hi, A x).PosDef
Tactic: by_cases h : ¬ hi.Nonempty
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ s, A i)
have 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)
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)
Cleared hypotheses: s, hs, hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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)
⊢ PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ s, A i)
have 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 i hi).Nonempty) (hA : ∀ i_1 ∈ insert i hi, (A i_1).PosDef),
  PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ insert i hi, 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)
Cleared hypotheses: s, hs, hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
⊢ PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ s, A i)
have 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)
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)
Cleared hypotheses: s, hs, hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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)
⊢ PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ s, A i)
have 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 i hi).Nonempty) (hA : ∀ i_1 ∈ insert i hi, (A i_1).PosDef),
  PosDef.{u_1, u_3} (n := m) (R := R) (∑ i ∈ insert i hi, 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)
Cleared hypotheses: s, hs, hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
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
have 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)
Tactic: refine ⟨IsSelfAdjoint.smul (IsSelfAdjoint.of_nonneg ha.le) hx.1, fun y hy => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix n m R
⊢ (Bᴴ * A * B).PosSemidef
have have : ∀ (this : Fintype m), (Bᴴ * A * B).PosSemidef
Tactic: have := Fintype.ofFinite m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : Finite m
A : Matrix n n R
hA : A.PosSemidef
B : Matrix n m R
this : Fintype m
⊢ (Bᴴ * A * B).PosSemidef
have refine : ∀ (x : m → R), 0 ≤ star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x
Tactic: refine of_dotProduct_mulVec_nonneg (isHermitian_conjTranspose_mul_mul B hA.1) fun x ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
n : Type u_2
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : Fintype n
inst_4 : StarOrderedRing R
inst_5 : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k_1 k : ℕ
⊢ (M ^ (k + 2)).PosSemidef
have rw : (M * M ^ k * M).PosSemidef
Tactic: rw [pow_succ, pow_succ']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
⊢ M⁻¹.PosSemidef
have pos : ∀ (h : IsUnit M.det), M⁻¹.PosSemidef
Tactic: by_cases h : IsUnit M.det
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
pos : ∀ (h : IsUnit M.det), M⁻¹.PosSemidef
⊢ M⁻¹.PosSemidef
have neg : ∀ (h : ¬IsUnit M.det), M⁻¹.PosSemidef
Tactic: by_cases h : IsUnit M.det
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (hypothesis)
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : IsUnit M.det
⊢ M⁻¹.PosSemidef
have this : (M⁻¹ᴴ * M * M⁻¹)ᴴ.PosSemidef
Tactic: have := (conjTranspose_mul_mul_same hM M⁻¹).conjTranspose
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : IsUnit M.det
this : (M⁻¹ᴴ * M * M⁻¹)ᴴ.PosSemidef
⊢ M⁻¹.PosSemidef
have pos : ∀ (this : M⁻¹ᴴᴴ.PosSemidef), M⁻¹.PosSemidef
Tactic: rwa [mul_nonsing_inv_cancel_right _ _ h, conjTranspose_conjTranspose] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : IsUnit M.det
this : (M⁻¹ᴴ * M * M⁻¹)ᴴ.PosSemidef
pos : ∀ (this : M⁻¹ᴴᴴ.PosSemidef), M⁻¹.PosSemidef
⊢ M⁻¹.PosSemidef
have pos₁ : ∀ (this : M⁻¹.PosSemidef), M⁻¹.PosSemidef
Tactic: rwa [mul_nonsing_inv_cancel_right _ _ h, conjTranspose_conjTranspose] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.PosDef (goal)
Goal:
n : Type u_2
R' : Type u_4
inst : CommRing R'
inst_1 : PartialOrder R'
inst_2 : StarRing R'
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : ¬IsUnit M.det
⊢ M⁻¹.PosSemidef
have neg : PosSemidef.{u_2, u_4} (n := n) (R := R') 0
Tactic: rw [nonsing_inv_apply_not_isUnit _ h]