awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
i : ι
hi : ¬v i = 0
contrapose : ∀ (hi : i ∉ s), v i = 0
⊢ i ∈ s

Tactic:
contrapose hi
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
i : ι
hi : i ∉ s
⊢ v i = 0

Tactic:
Pi.mem_spanSubset_iff.mp hv i hi

Premises used: Pi.mem_spanSubset_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
i : ι
hi : i ∉ s
⊢ v i = 0

Tactic:
exact Pi.mem_spanSubset_iff.mp hv i hi

Premises used: Pi.mem_spanSubset_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
i : ι
hi : ¬v i = 0
⊢ i ∈ s

Tactic:
have : i ∈ s := by
      contrapose hi
      exact Pi.mem_spanSubset_iff.mp hv i hi
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
i : ι
hi : ¬v i = 0
this : i ∈ s
⊢ 0 <
    w i •
      ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i *
        (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i)

Tactic:
smul_pos (hs i this) (mul_self_pos.mpr hi)

Premises used: Iff.mpr, mul_self_pos, smul_pos
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) v
i : ι
hi : ¬v i = 0
this : i ∈ s
⊢ 0 <
    w i •
      ((↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i *
        (↑(Subtype.mk (p := fun (x : ι → 𝕜) ↦ Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x) v hv) :
            ι → 𝕜)
          i)

Tactic:
exact smul_pos (hs i this) (mul_self_pos.mpr hi)

Premises used: Iff.mpr, mul_self_pos, smul_pos
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x
simp : LE.le.{u_4} (α := 𝕜) (∑ x_1 : ι, w x_1 * (x x_1 * x x_1)) 0
⊢ LE.le.{u_4} (α := 𝕜) ((weightedSumSquares 𝕜 w : (a : ι → 𝕜) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
simp only [weightedSumSquares_apply, smul_eq_mul]

Premises used: QuadraticMap.weightedSumSquares_apply, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x
h : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → w i * (x i * x i) ≤ 0
⊢ LE.le.{u_4} (α := 𝕜) (∑ x_1 : ι, w x_1 * (x x_1 * x x_1)) 0

Tactic:
apply sum_nonpos

Premises used: Finset.sum_nonpos
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x
i : ι
h : Membership.mem (γ := Finset ι) univ i → w i * (x i * x i) ≤ 0
⊢ Membership.mem (γ := Finset ι) univ i → w i * (x i * x i) ≤ 0

Tactic:
_
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x
i : ι
h : Membership.mem (γ := Finset ι) univ i
pos : ∀ (hi : i ∈ s), w i * (x i * x i) ≤ 0
neg : ∀ (hi : i ∉ s), w i * (x i * x i) ≤ 0
⊢ w i * (x i * x i) ≤ 0

Tactic:
by_cases hi : i ∈ s
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x
i : ι
h : Membership.mem (γ := Finset ι) univ i
hi : i ∈ s
⊢ w i * (x i * x i) ≤ 0

Tactic:
mul_nonpos_of_nonpos_of_nonneg (hs i hi) (mul_self_nonneg _)

Premises used: mul_self_nonneg, mul_nonpos_of_nonpos_of_nonneg
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x
i : ι
h : Membership.mem (γ := Finset ι) univ i
hi : i ∈ s
⊢ w i * (x i * x i) ≤ 0

Tactic:
exact mul_nonpos_of_nonpos_of_nonneg (hs i hi) (mul_self_nonneg _)

Premises used: mul_self_nonneg, mul_nonpos_of_nonpos_of_nonneg
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : Membership.mem (γ := Submodule 𝕜 (ι → 𝕜)) (Pi.spanSubset 𝕜 s) x
i : ι
h : Membership.mem (γ := Finset ι) univ i
hi : i ∉ s
neg : w i * HMul.hMul (α := 𝕜) 0 0 ≤ 0
neg₁ : w i * 0 ≤ 0
neg₂ neg₃ : LE.le.{u_4} (α := 𝕜) 0 0
⊢ w i * (x i * x i) ≤ 0

Tactic:
rw [Pi.mem_spanSubset_iff.mp hx i hi, mul_zero, mul_zero]

Premises used: Pi.mem_spanSubset_iff, MulZeroClass.mul_zero, Iff.mp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
p : Set ι := {i : ι | 0 < w i}
m : Set ι := {i : ι | w i ≤ 0}
convert_8 : sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = p.ncard
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i}

Tactic:
convert_to sigPos _ = p.ncard

Premises used: sigPos, Set.ncard
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
p : Set ι := {i : ι | 0 < w i}
m : Set ι := {i : ι | w i ≤ 0}
⊢ p.ncard + pᶜ.ncard = Nat.card ι

Tactic:
Set.ncard_add_ncard_compl p

Premises used: Set.ncard_add_ncard_compl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
p : Set ι := {i : ι | 0 < w i}
m : Set ι := {i : ι | w i ≤ 0}
h : m = pᶜ
⊢ p.ncard + m.ncard = Nat.card ι

Tactic:
convert! Set.ncard_add_ncard_compl p

Premises used: Set.ncard_add_ncard_compl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
p : Set ι := {i : ι | 0 < w i}
m : Set ι := {i : ι | w i ≤ 0}
h : ∀ (x : ι), x ∈ m ↔ x ∈ pᶜ
⊢ m = pᶜ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
p : Set ι := {i : ι | 0 < w i}
m : Set ι := {i : ι | w i ≤ 0}
x : ι
⊢ x ∈ m ↔ x ∈ pᶜ

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
p : Set ι := {i : ι | 0 < w i}
m : Set ι := {i : ι | w i ≤ 0}
⊢ p.ncard + m.ncard = Nat.card ι

Tactic:
have : p.ncard + m.ncard = Nat.card ι := by
    convert! Set.ncard_add_ncard_compl p
    ext
    grind
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
p : Set ι := {i : ι | 0 < w i}
m : Set ι := {i : ι | w i ≤ 0}
this : p.ncard + m.ncard = Nat.card ι
⊢ ∀ i ∈ p, 0 < w i

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
p : Set ι := {i : ι | 0 < w i}
m : Set ι := {i : ι | w i ≤ 0}
this : p.ncard + m.ncard = Nat.card ι
⊢ p.ncard ≤ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w)

Tactic:
have : p.ncard ≤ sigPos (weightedSumSquares 𝕜 w) :=
    (sigPos_isGreatest _).2 ⟨Pi.spanSubset 𝕜 p, Pi.dim_spanSubset,
      posDef_spanSubset p (by grind)⟩
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
p : Set ι := {i : ι | 0 < w i}
m : Set ι := {i : ι | w i ≤ 0}
this_1 : p.ncard + m.ncard = Nat.card ι
this_2 : p.ncard ≤ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w)
this : sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + m.ncard ≤ Nat.card ι
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = p.ncard

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
p : Set ι := {i : ι | 0 < w i}
m : Set ι := {i : ι | w i ≤ 0}
this_1 : p.ncard + m.ncard = Nat.card ι
this : p.ncard ≤ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w)
convert_8 : sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + m.ncard ≤ Nat.card ι
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = p.ncard

Tactic:
suffices sigPos (weightedSumSquares 𝕜 w) + m.ncard ≤ Nat.card ι by lia
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
p : Set ι := {i : ι | 0 < w i}
m : Set ι := {i : ι | w i ≤ 0}
this_1 : p.ncard + m.ncard = Nat.card ι
this : p.ncard ≤ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w)
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + m.ncard ≤ Nat.card ι

Tactic:
simpa using sigPos_add_finrank_le_of_nonpos <| negSemidef_spanSubset m (fun _ hi ↦ hi)

Premises used: _private.0.QuadraticForm.negSemidef_spanSubset, QuadraticForm.sigPos_add_finrank_le_of_nonpos
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
let let₁ let₂ let₃ : sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i}
convert_8 :
  let p : Set ι := {i : ι | 0 < w i};
  sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = p.ncard
convert_8₁ :
  let p : Set ι := {i : ι | 0 < w i};
  let m : Set ι := {i : ι | w i ≤ 0};
  ∀ (this : p.ncard + m.ncard = Nat.card ι), sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = p.ncard
convert_8₂ :
  let p : Set ι := {i : ι | 0 < w i};
  let m : Set ι := {i : ι | w i ≤ 0};
  ∀ (this : p.ncard + m.ncard = Nat.card ι) (this : p.ncard ≤ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w)),
    sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = p.ncard
convert_8₃ :
  let p : Set ι := {i : ι | 0 < w i};
  let m : Set ι := {i : ι | w i ≤ 0};
  ∀ (this : p.ncard + m.ncard = Nat.card ι) (this : p.ncard ≤ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w)),
    sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + m.ncard ≤ Nat.card ι
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i}

Tactic:
classical
  let p : Set ι := {i | 0 < w i}
  let m : Set ι := {i | w i ≤ 0}
  convert_to sigPos _ = p.ncard
  have : p.ncard + m.ncard = Nat.card ι := by
    convert! Set.ncard_add_ncard_compl p
    ext
    grind
  have : p.ncard ≤ sigPos (weightedSumSquares 𝕜 w) :=
    (sigPos_isGreatest _).2 ⟨Pi.spanSubset 𝕜 p, Pi.dim_spanSubset,
      posDef_spanSubset p (by grind)⟩
  suffices sigPos (weightedSumSquares 𝕜 w) + m.ncard ≤ Nat.card ι by lia
  simpa using sigPos_add_finrank_le_of_nonpos <| negSemidef_spanSubset m (fun _ hi ↦ hi)

Premises used: sigPos, QuadraticForm.sigPos_add_finrank_le_of_nonpos
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 (-w)) = Set.ncard.{u_5} (α := ι) {i : ι | 0 < (-w) i}

Tactic:
sigPos_weightedSumSquares (w := -w)

Premises used: QuadraticForm.sigPos_weightedSumSquares
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
h : Eq (α := QuadraticForm 𝕜 (ι → 𝕜)) (-weightedSumSquares 𝕜 w) (weightedSumSquares 𝕜 (-w))
h₁ : Eq.{u_5 + 1} (α := Set ι) {i : ι | w i < 0} {i : ι | 0 < (-w) i}
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (-weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | w i < 0}

Tactic:
convert! sigPos_weightedSumSquares (w := -w) using 2

Premises used: QuadraticForm.sigPos_weightedSumSquares
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
h :
  ∀ (x : ι → 𝕜),
    Eq.{u_4 + 1} (α := 𝕜) ((-weightedSumSquares 𝕜 w : (a : ι → 𝕜) → 𝕜) x : 𝕜)
      ((weightedSumSquares 𝕜 (-w) : (a : ι → 𝕜) → 𝕜) x : 𝕜)
⊢ Eq (α := QuadraticForm 𝕜 (ι → 𝕜)) (-weightedSumSquares 𝕜 w) (weightedSumSquares 𝕜 (-w))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
x : ι → 𝕜
⊢ Eq.{u_4 + 1} (α := 𝕜) ((-weightedSumSquares 𝕜 w : (a : ι → 𝕜) → 𝕜) x : 𝕜)
    ((weightedSumSquares 𝕜 (-w) : (a : ι → 𝕜) → 𝕜) x : 𝕜)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ Eq.{u_5 + 1} (α := Set ι) {i : ι | w i < 0} {i : ι | 0 < (-w) i}

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
rw :
  Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i < 0} +
      Set.ncard.{u_5} (α := ι) {i : ι | w i = 0} =
    Nat.card ι
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜 ↥(radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) =
    Nat.card ι

Tactic:
rw [radical_weightedSumSquares, sigPos_weightedSumSquares, sigNeg_weightedSumSquares,
    Pi.dim_spanSubset]

Premises used: QuadraticForm.sigNeg_weightedSumSquares, QuadraticForm.sigPos_weightedSumSquares, Pi.dim_spanSubset, QuadraticForm.radical_weightedSumSquares
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
rw : Set.ncard.{u_5} (α := ι) ({i : ι | w i < 0} ∪ {i : ι | w i = 0}) = Set.ncard.{u_5} (α := ι) {i : ι | w i ≤ 0}
rw₁ : Disjoint.{u_5} (α := Set ι) {i : ι | w i < 0} {i : ι | w i = 0}
⊢ Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i < 0} +
      Set.ncard.{u_5} (α := ι) {i : ι | w i = 0} =
    Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i ≤ 0}

Tactic:
rw [add_assoc, add_left_cancel_iff, ← Set.ncard_union_eq]

Premises used: add_assoc, Set.ncard_union_eq, add_left_cancel_iff
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
h : Eq.{u_5 + 1} (α := Set ι) ({i : ι | w i < 0} ∪ {i : ι | w i = 0}) {i : ι | w i ≤ 0}
⊢ Set.ncard.{u_5} (α := ι) ({i : ι | w i < 0} ∪ {i : ι | w i = 0}) = Set.ncard.{u_5} (α := ι) {i : ι | w i ≤ 0}

Tactic:
congr! 1
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
h :
  ∀ (x : ι),
    Membership.mem (γ := Set ι) ({i : ι | w i < 0} ∪ {i : ι | w i = 0}) x ↔
      Membership.mem (γ := Set ι) {i : ι | w i ≤ 0} x
⊢ Eq.{u_5 + 1} (α := Set ι) ({i : ι | w i < 0} ∪ {i : ι | w i = 0}) {i : ι | w i ≤ 0}

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
x : ι
⊢ Membership.mem (γ := Set ι) ({i : ι | w i < 0} ∪ {i : ι | w i = 0}) x ↔
    Membership.mem (γ := Set ι) {i : ι | w i ≤ 0} x

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ Disjoint.{u_5} (α := Set ι) {i : ι | w i < 0} {i : ι | w i = 0}

Tactic:
grind [disjoint_iff_ne]

Premises used: Finset.disjoint_iff_ne
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
rw : Set.ncard.{u_5} (α := ι) ({i : ι | 0 < w i} ∪ {i : ι | w i ≤ 0}) = Set.ncard.{u_5} (α := ι) Set.univ
rw₁ : Disjoint.{u_5} (α := Set ι) {i : ι | 0 < w i} {i : ι | w i ≤ 0}
⊢ Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i ≤ 0} =
    Set.ncard.{u_5} (α := ι) Set.univ

Tactic:
rw [← Set.ncard_union_eq]

Premises used: Set.ncard_union_eq
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
h : Eq.{u_5 + 1} (α := Set ι) ({i : ι | 0 < w i} ∪ {i : ι | w i ≤ 0}) Set.univ
⊢ Set.ncard.{u_5} (α := ι) ({i : ι | 0 < w i} ∪ {i : ι | w i ≤ 0}) = Set.ncard.{u_5} (α := ι) Set.univ

Tactic:
congr! 1
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
h :
  ∀ (x : ι),
    Membership.mem (γ := Set ι) ({i : ι | 0 < w i} ∪ {i : ι | w i ≤ 0}) x ↔ Membership.mem (γ := Set ι) Set.univ x
⊢ Eq.{u_5 + 1} (α := Set ι) ({i : ι | 0 < w i} ∪ {i : ι | w i ≤ 0}) Set.univ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
x : ι
⊢ Membership.mem (γ := Set ι) ({i : ι | 0 < w i} ∪ {i : ι | w i ≤ 0}) x ↔ Membership.mem (γ := Set ι) Set.univ x

Tactic:
grind [le_iff_lt_or_eq]

Premises used: le_iff_lt_or_eq
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ Disjoint.{u_5} (α := Set ι) {i : ι | 0 < w i} {i : ι | w i ≤ 0}

Tactic:
grind [disjoint_iff_ne]

Premises used: Finset.disjoint_iff_ne
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ Set.ncard.{u_5} (α := ι) Set.univ = Nat.card ι

Tactic:
Set.ncard_univ _

Premises used: Set.ncard_univ
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
calc :
  Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i < 0} +
      Set.ncard.{u_5} (α := ι) {i : ι | w i = 0} =
    Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i ≤ 0}
calc₁ :
  Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i ≤ 0} =
    Set.ncard.{u_5} (α := ι) Set.univ
⊢ Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i < 0} +
      Set.ncard.{u_5} (α := ι) {i : ι | w i = 0} =
    Nat.card ι

Tactic:
calc {i | 0 < w i}.ncard + {i | w i < 0}.ncard + {i | w i = 0}.ncard
  _ = {i | 0 < w i}.ncard + {i | w i ≤ 0}.ncard := by
    rw [add_assoc, add_left_cancel_iff, ← Set.ncard_union_eq]
    · congr! 1
      ext
      grind
    · grind [disjoint_iff_ne]
  _ = Set.univ.ncard := by
    rw [← Set.ncard_union_eq]
    · congr! 1
      ext
      grind [le_iff_lt_or_eq]
    · grind [disjoint_iff_ne]
  _ = Nat.card ι := Set.ncard_univ _

Premises used: Set.univ, setOf, Nat.card, LE.le, LT.lt, Set.ncard_univ, Set.ncard, OfNat.ofNat, Eq
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
rw :
  sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜 ↥(Pi.spanSubset 𝕜 {i : ι | w i = 0}) =
    Nat.card ι
rw₁ :
  Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜 ↥(Pi.spanSubset 𝕜 {i : ι | w i = 0}) =
    Nat.card ι
rw₂ :
  Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i < 0} +
      Module.finrank 𝕜 ↥(Pi.spanSubset 𝕜 {i : ι | w i = 0}) =
    Nat.card ι
rw₃ rw₄ rw₅ :
  Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i < 0} +
      Set.ncard.{u_5} (α := ι) {i : ι | w i = 0} =
    Nat.card ι
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜 ↥(radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) =
    Nat.card ι

Tactic:
classical
  rw [radical_weightedSumSquares, sigPos_weightedSumSquares, sigNeg_weightedSumSquares,
    Pi.dim_spanSubset]
  calc {i | 0 < w i}.ncard + {i | w i < 0}.ncard + {i | w i = 0}.ncard
  _ = {i | 0 < w i}.ncard + {i | w i ≤ 0}.ncard := by
    rw [add_assoc, add_left_cancel_iff, ← Set.ncard_union_eq]
    · congr! 1
      ext
      grind
    · grind [disjoint_iff_ne]
  _ = Set.univ.ncard := by
    rw [← Set.ncard_union_eq]
    · congr! 1
      ext
      grind [le_iff_lt_or_eq]
    · grind [disjoint_iff_ne]
  _ = Nat.card ι := Set.ncard_univ _

Premises used: Set.univ, setOf, Nat.card, LE.le, QuadraticForm.sigNeg_weightedSumSquares, QuadraticForm.sigPos_weightedSumSquares, LT.lt, Pi.dim_spanSubset, QuadraticForm.radical_weightedSumSquares, Set.ncard_univ, Set.ncard, OfNat.ofNat, Eq