awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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
⊢ w i * (x i * x i) ≤ 0
have neg₁ : w i * 0 ≤ 0
Tactic: rw [Pi.mem_spanSubset_iff.mp hx i hi, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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
⊢ w i * (x i * x i) ≤ 0
have neg₂ : LE.le.{u_4} (α := 𝕜) 0 0
Tactic: rw [Pi.mem_spanSubset_iff.mp hx i hi, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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 ι
have h : m = pᶜ
Tactic: convert! Set.ncard_add_ncard_compl p
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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}
⊢ m = pᶜ
have h : ∀ (x : ι), x ∈ m ↔ x ∈ pᶜ
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (hypothesis)
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}
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = p.ncard
have this : p.ncard + m.ncard = Nat.card ι
Tactic: have : p.ncard + m.ncard = Nat.card ι := by
    convert! Set.ncard_add_ncard_compl p
    ext
    grind
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (hypothesis)
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 ι
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = p.ncard
have this₁ : 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)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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) = p.ncard
have convert_8 : sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + m.ncard ≤ Nat.card ι
Tactic: suffices sigPos (weightedSumSquares 𝕜 w) + m.ncard ≤ Nat.card ι by lia
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i}
have 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
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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i}
have 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
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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i}
have 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 ι
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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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 : ι | w i < 0}
have h : Eq (α := QuadraticForm 𝕜 (ι → 𝕜)) (-weightedSumSquares 𝕜 w) (weightedSumSquares 𝕜 (-w))
Tactic: convert! sigPos_weightedSumSquares (w := -w) using 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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))
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (-weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | w i < 0}
have h₁ : Eq.{u_5 + 1} (α := Set ι) {i : ι | w i < 0} {i : ι | 0 < (-w) i}
Tactic: convert! sigPos_weightedSumSquares (w := -w) using 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ Eq (α := QuadraticForm 𝕜 (ι → 𝕜)) (-weightedSumSquares 𝕜 w) (weightedSumSquares 𝕜 (-w))
have h : ∀ (x : ι → 𝕜),
  Eq.{u_4 + 1} (α := 𝕜) ((-weightedSumSquares 𝕜 w : (a : ι → 𝕜) → 𝕜) x : 𝕜)
    ((weightedSumSquares 𝕜 (-w) : (a : ι → 𝕜) → 𝕜) x : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜 ↥(radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) =
    Nat.card ι
have 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 ι
Tactic: rw [radical_weightedSumSquares, sigPos_weightedSumSquares, sigNeg_weightedSumSquares,
    Pi.dim_spanSubset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ 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}
have rw : Set.ncard.{u_5} (α := ι) ({i : ι | w i < 0} ∪ {i : ι | w i = 0}) = Set.ncard.{u_5} (α := ι) {i : ι | w i ≤ 0}
Tactic: rw [add_assoc, add_left_cancel_iff, ← Set.ncard_union_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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}
⊢ 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}
have rw₁ : Disjoint.{u_5} (α := Set ι) {i : ι | w i < 0} {i : ι | w i = 0}
Tactic: rw [add_assoc, add_left_cancel_iff, ← Set.ncard_union_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ Set.ncard.{u_5} (α := ι) ({i : ι | w i < 0} ∪ {i : ι | w i = 0}) = Set.ncard.{u_5} (α := ι) {i : ι | w i ≤ 0}
have h : Eq.{u_5 + 1} (α := Set ι) ({i : ι | w i < 0} ∪ {i : ι | w i = 0}) {i : ι | w i ≤ 0}
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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 : ι | w i = 0}) {i : ι | w i ≤ 0}
have h : ∀ (x : ι),
  Membership.mem (γ := Set ι) ({i : ι | w i < 0} ∪ {i : ι | w i = 0}) x ↔
    Membership.mem (γ := Set ι) {i : ι | w i ≤ 0} x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i ≤ 0} =
    Set.ncard.{u_5} (α := ι) Set.univ
have rw : Set.ncard.{u_5} (α := ι) ({i : ι | 0 < w i} ∪ {i : ι | w i ≤ 0}) = Set.ncard.{u_5} (α := ι) Set.univ
Tactic: rw [← Set.ncard_union_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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
⊢ Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i ≤ 0} =
    Set.ncard.{u_5} (α := ι) Set.univ
have rw₁ : Disjoint.{u_5} (α := Set ι) {i : ι | 0 < w i} {i : ι | w i ≤ 0}
Tactic: rw [← Set.ncard_union_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ Set.ncard.{u_5} (α := ι) ({i : ι | 0 < w i} ∪ {i : ι | w i ≤ 0}) = Set.ncard.{u_5} (α := ι) Set.univ
have h : Eq.{u_5 + 1} (α := Set ι) ({i : ι | 0 < w i} ∪ {i : ι | w i ≤ 0}) Set.univ
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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 : ι | 0 < w i} ∪ {i : ι | w i ≤ 0}) Set.univ
have h : ∀ (x : ι),
  Membership.mem (γ := Set ι) ({i : ι | 0 < w i} ∪ {i : ι | w i ≤ 0}) x ↔ Membership.mem (γ := Set ι) Set.univ x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ 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 ι
have 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}
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 _
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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}
⊢ 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 ι
have calc₁ : Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + Set.ncard.{u_5} (α := ι) {i : ι | w i ≤ 0} =
  Set.ncard.{u_5} (α := ι) Set.univ
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 _
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
ι : Type u_5
inst_2 : Fintype ι
w : ι → 𝕜
inst_3 : IsStrictOrderedRing 𝕜
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜 ↥(radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) =
    Nat.card ι
have rw : sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) +
    Module.finrank 𝕜 ↥(Pi.spanSubset 𝕜 {i : ι | w i = 0}) =
  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 _
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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 ι
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜 ↥(radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) =
    Nat.card ι
have rw₁ : Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i} + sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) +
    Module.finrank 𝕜 ↥(Pi.spanSubset 𝕜 {i : ι | w i = 0}) =
  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 _
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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 ι
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜 ↥(radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) =
    Nat.card ι
have 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 ι
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 _
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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 ι
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) + sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜 ↥(radical (R := 𝕜) (M := ι → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) : Submodule 𝕜 (ι → 𝕜)) =
    Nat.card ι
have 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 ι
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 _
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : IsStrictOrderedRing 𝕜
inst_5 : FiniteDimensional 𝕜 M
⊢ sigPos Q + sigNeg Q + Module.finrank.{u_4, u_2} 𝕜 ↥(radical (P := 𝕜) Q) = Module.finrank 𝕜 M
have have : ∀ (this : Invertible (α := 𝕜) 2),
  sigPos Q + sigNeg Q + Module.finrank.{u_4, u_2} 𝕜 ↥(radical (P := 𝕜) Q) = Module.finrank 𝕜 M
Tactic: have : Invertible (2 : 𝕜) := invertibleOfNonzero (NeZero.ne _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : IsStrictOrderedRing 𝕜
inst_5 : FiniteDimensional 𝕜 M
this : Invertible (α := 𝕜) 2
⊢ sigPos Q + sigNeg Q + Module.finrank.{u_4, u_2} 𝕜 ↥(radical (P := 𝕜) Q) = Module.finrank 𝕜 M
have obtain : ∀ (w : Fin (Module.finrank 𝕜 M) → 𝕜) (e : Equivalent Q (weightedSumSquares 𝕜 w)),
  sigPos Q + sigNeg Q + Module.finrank.{u_4, u_2} 𝕜 ↥(radical (P := 𝕜) Q) = Module.finrank 𝕜 M
Tactic: obtain ⟨w, e⟩ := Q.equivalent_weightedSumSquares