[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
⊢ ∑ x : σ → K, ↑(eval x) f = 0
[PROOFSTEP]
haveI : DecidableEq K := Classical.decEq K
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
⊢ ∑ x : σ → K, ↑(eval x) f = 0
[PROOFSTEP]
calc
  ∑ x, eval x f = ∑ x : σ → K, ∑ d in f.support, f.coeff d * ∏ i, x i ^ d i := by simp only [eval_eq']
  _ = ∑ d in f.support, ∑ x : σ → K, f.coeff d * ∏ i, x i ^ d i := sum_comm
  _ = 0 := sum_eq_zero ?_
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
⊢ ∑ x : σ → K, ↑(eval x) f = ∑ x : σ → K, ∑ d in support f, coeff d f * ∏ i : σ, x i ^ ↑d i
[PROOFSTEP]
simp only [eval_eq']
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
⊢ ∀ (x : σ →₀ ℕ), x ∈ support f → ∑ x_1 : σ → K, coeff x f * ∏ i : σ, x_1 i ^ ↑x i = 0
[PROOFSTEP]
intro d hd
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
⊢ ∑ x : σ → K, coeff d f * ∏ i : σ, x i ^ ↑d i = 0
[PROOFSTEP]
obtain ⟨i, hi⟩ : ∃ i, d i < q - 1
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
⊢ ∃ i, ↑d i < q - 1
case intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
⊢ ∑ x : σ → K, coeff d f * ∏ i : σ, x i ^ ↑d i = 0
[PROOFSTEP]
exact f.exists_degree_lt (q - 1) h hd
[GOAL]
case intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
⊢ ∑ x : σ → K, coeff d f * ∏ i : σ, x i ^ ↑d i = 0
[PROOFSTEP]
calc
  (∑ x : σ → K, f.coeff d * ∏ i, x i ^ d i) = f.coeff d * ∑ x : σ → K, ∏ i, x i ^ d i := mul_sum.symm
  _ = 0 := (mul_eq_zero.mpr ∘ Or.inr) ?_
[GOAL]
case intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
⊢ ∑ x : σ → K, ∏ i : σ, x i ^ ↑d i = 0
[PROOFSTEP]
calc
  (∑ x : σ → K, ∏ i, x i ^ d i) =
      ∑ x₀ : { j // j ≠ i } → K, ∑ x : { x : σ → K // x ∘ (↑) = x₀ }, ∏ j, (x : σ → K) j ^ d j :=
    (Fintype.sum_fiberwise _ _).symm
  _ = 0 := Fintype.sum_eq_zero _ ?_
[GOAL]
case intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
⊢ ∀ (a : { j // j ≠ i } → K), ∑ x : { x // x ∘ Subtype.val = a }, ∏ j : σ, ↑x j ^ ↑d j = 0
[PROOFSTEP]
intro x₀
[GOAL]
case intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
⊢ ∑ x : { x // x ∘ Subtype.val = x₀ }, ∏ j : σ, ↑x j ^ ↑d j = 0
[PROOFSTEP]
let e : K ≃ { x // x ∘ ((↑) : _ → σ) = x₀ } := (Equiv.subtypeEquivCodomain _).symm
[GOAL]
case intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ ∑ x : { x // x ∘ Subtype.val = x₀ }, ∏ j : σ, ↑x j ^ ↑d j = 0
[PROOFSTEP]
calc
  (∑ x : { x : σ → K // x ∘ (↑) = x₀ }, ∏ j, (x : σ → K) j ^ d j) = ∑ a : K, ∏ j : σ, (e a : σ → K) j ^ d j :=
    (e.sum_comp _).symm
  _ = ∑ a : K, (∏ j, x₀ j ^ d j) * a ^ d i := (Fintype.sum_congr _ _ ?_)
  _ = (∏ j, x₀ j ^ d j) * ∑ a : K, a ^ d i := by rw [mul_sum]
  _ = 0 := by rw [sum_pow_lt_card_sub_one K _ hi, mul_zero]
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ ∑ a : K, (∏ j : { j // j ≠ i }, x₀ j ^ ↑d ↑j) * a ^ ↑d i = (∏ j : { j // j ≠ i }, x₀ j ^ ↑d ↑j) * ∑ a : K, a ^ ↑d i
[PROOFSTEP]
rw [mul_sum]
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ (∏ j : { j // j ≠ i }, x₀ j ^ ↑d ↑j) * ∑ a : K, a ^ ↑d i = 0
[PROOFSTEP]
rw [sum_pow_lt_card_sub_one K _ hi, mul_zero]
[GOAL]
case intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ ∀ (a : K), ∏ j : σ, ↑(↑e a) j ^ ↑d j = (∏ j : { j // j ≠ i }, x₀ j ^ ↑d ↑j) * a ^ ↑d i
[PROOFSTEP]
intro a
[GOAL]
case intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
⊢ ∏ j : σ, ↑(↑e a) j ^ ↑d j = (∏ j : { j // j ≠ i }, x₀ j ^ ↑d ↑j) * a ^ ↑d i
[PROOFSTEP]
let e' : Sum { j // j = i } { j // j ≠ i } ≃ σ := Equiv.sumCompl _
[GOAL]
case intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j => j = i
⊢ ∏ j : σ, ↑(↑e a) j ^ ↑d j = (∏ j : { j // j ≠ i }, x₀ j ^ ↑d ↑j) * a ^ ↑d i
[PROOFSTEP]
letI : Unique { j // j = i } :=
  { default := ⟨i, rfl⟩
    uniq := fun ⟨j, h⟩ => Subtype.val_injective h }
[GOAL]
case intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j => j = i
this : Unique { j // j = i } :=
  { toInhabited := { default := { val := i, property := (_ : i = i) } },
    uniq := (_ : ∀ (x : { j // j = i }), x = default) }
⊢ ∏ j : σ, ↑(↑e a) j ^ ↑d j = (∏ j : { j // j ≠ i }, x₀ j ^ ↑d ↑j) * a ^ ↑d i
[PROOFSTEP]
calc
  (∏ j : σ, (e a : σ → K) j ^ d j) = (e a : σ → K) i ^ d i * ∏ j : { j // j ≠ i }, (e a : σ → K) j ^ d j := by
    rw [← e'.prod_comp, Fintype.prod_sum_type, univ_unique, prod_singleton]; rfl
  _ = a ^ d i * ∏ j : { j // j ≠ i }, (e a : σ → K) j ^ d j := by rw [Equiv.subtypeEquivCodomain_symm_apply_eq]
  _ = a ^ d i * ∏ j, x₀ j ^ d j :=
    (congr_arg _ (Fintype.prod_congr _ _ ?_))
      -- see below
  _ = (∏ j, x₀ j ^ d j) * a ^ d i := mul_comm _ _
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j => j = i
this : Unique { j // j = i } :=
  { toInhabited := { default := { val := i, property := (_ : i = i) } },
    uniq := (_ : ∀ (x : { j // j = i }), x = default) }
⊢ ∏ j : σ, ↑(↑e a) j ^ ↑d j = ↑(↑e a) i ^ ↑d i * ∏ j : { j // j ≠ i }, ↑(↑e a) ↑j ^ ↑d ↑j
[PROOFSTEP]
rw [← e'.prod_comp, Fintype.prod_sum_type, univ_unique, prod_singleton]
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j => j = i
this : Unique { j // j = i } :=
  { toInhabited := { default := { val := i, property := (_ : i = i) } },
    uniq := (_ : ∀ (x : { j // j = i }), x = default) }
⊢ ↑(↑e a) (↑e' (Sum.inl default)) ^ ↑d (↑e' (Sum.inl default)) *
      ∏ a₂ : { j // j ≠ i }, ↑(↑e a) (↑e' (Sum.inr a₂)) ^ ↑d (↑e' (Sum.inr a₂)) =
    ↑(↑e a) i ^ ↑d i * ∏ j : { j // j ≠ i }, ↑(↑e a) ↑j ^ ↑d ↑j
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j => j = i
this : Unique { j // j = i } :=
  { toInhabited := { default := { val := i, property := (_ : i = i) } },
    uniq := (_ : ∀ (x : { j // j = i }), x = default) }
⊢ ↑(↑e a) i ^ ↑d i * ∏ j : { j // j ≠ i }, ↑(↑e a) ↑j ^ ↑d ↑j = a ^ ↑d i * ∏ j : { j // j ≠ i }, ↑(↑e a) ↑j ^ ↑d ↑j
[PROOFSTEP]
rw [Equiv.subtypeEquivCodomain_symm_apply_eq]
[GOAL]
case intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j => j = i
this : Unique { j // j = i } :=
  { toInhabited := { default := { val := i, property := (_ : i = i) } },
    uniq := (_ : ∀ (x : { j // j = i }), x = default) }
⊢ ∀ (a_1 : { j // j ≠ i }), ↑(↑e a) ↑a_1 ^ ↑d ↑a_1 = x₀ a_1 ^ ↑d ↑a_1
[PROOFSTEP]
rintro ⟨j, hj⟩
[GOAL]
case intro.mk
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j => j = i
this : Unique { j // j = i } :=
  { toInhabited := { default := { val := i, property := (_ : i = i) } },
    uniq := (_ : ∀ (x : { j // j = i }), x = default) }
j : σ
hj : j ≠ i
⊢ ↑(↑e a) ↑{ val := j, property := hj } ^ ↑d ↑{ val := j, property := hj } =
    x₀ { val := j, property := hj } ^ ↑d ↑{ val := j, property := hj }
[PROOFSTEP]
show (e a : σ → K) j ^ d j = x₀ ⟨j, hj⟩ ^ d j
[GOAL]
case intro.mk
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : totalDegree f < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ support f
i : σ
hi : ↑d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j => j = i
this : Unique { j // j = i } :=
  { toInhabited := { default := { val := i, property := (_ : i = i) } },
    uniq := (_ : ∀ (x : { j // j = i }), x = default) }
j : σ
hj : j ≠ i
⊢ ↑(↑e a) j ^ ↑d j = x₀ { val := j, property := hj } ^ ↑d j
[PROOFSTEP]
rw [Equiv.subtypeEquivCodomain_symm_apply_ne]
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
⊢ p ∣ Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 }
[PROOFSTEP]
have hq : 0 < q - 1 := by rw [← Fintype.card_units, Fintype.card_pos_iff]; exact ⟨1⟩
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
⊢ 0 < q - 1
[PROOFSTEP]
rw [← Fintype.card_units, Fintype.card_pos_iff]
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
⊢ Nonempty Kˣ
[PROOFSTEP]
exact ⟨1⟩
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
⊢ p ∣ Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 }
[PROOFSTEP]
let S : Finset (σ → K) := {x ∈ univ | ∀ i ∈ s, eval x (f i) = 0}.toFinset
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
⊢ p ∣ Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 }
[PROOFSTEP]
have hS : ∀ x : σ → K, x ∈ S ↔ ∀ i : ι, i ∈ s → eval x (f i) = 0 :=
  by
  intro x
  simp only [Set.toFinset_setOf, mem_univ, true_and, mem_filter]
    /- The polynomial `F = ∏ i in s, (1 - (f i)^(q - 1))` has the nice property
        that it takes the value `1` on elements of `{x : σ → K // ∀ i ∈ s, (f i).eval x = 0}`
        while it is `0` outside that locus.
        Hence the sum of its values is equal to the cardinality of
        `{x : σ → K // ∀ i ∈ s, (f i).eval x = 0}` modulo `p`. -/
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
⊢ ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
[PROOFSTEP]
intro x
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
x : σ → K
⊢ x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
[PROOFSTEP]
simp only [Set.toFinset_setOf, mem_univ, true_and, mem_filter]
  /- The polynomial `F = ∏ i in s, (1 - (f i)^(q - 1))` has the nice property
      that it takes the value `1` on elements of `{x : σ → K // ∀ i ∈ s, (f i).eval x = 0}`
      while it is `0` outside that locus.
      Hence the sum of its values is equal to the cardinality of
      `{x : σ → K // ∀ i ∈ s, (f i).eval x = 0}` modulo `p`. -/
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
⊢ p ∣ Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 }
[PROOFSTEP]
let F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
⊢ p ∣ Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 }
[PROOFSTEP]
have hF : ∀ x, eval x F = if x ∈ S then 1 else 0 := by
  intro x
  calc
    eval x F = ∏ i in s, eval x (1 - f i ^ (q - 1)) := eval_prod s _ x
    _ = if x ∈ S then 1 else 0 := ?_
  simp only [(eval x).map_sub, (eval x).map_pow, (eval x).map_one]
  split_ifs with hx
  · apply Finset.prod_eq_one
    intro i hi
    rw [hS] at hx 
    rw [hx i hi, zero_pow hq, sub_zero]
  · obtain ⟨i, hi, hx⟩ : ∃ i : ι, i ∈ s ∧ eval x (f i) ≠ 0 := by simpa only [hS, not_forall, not_imp] using hx
    apply Finset.prod_eq_zero hi
    rw [pow_card_sub_one_eq_one (eval x (f i)) hx, sub_self]
      -- In particular, we can now show:
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
⊢ ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
[PROOFSTEP]
intro x
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
x : σ → K
⊢ ↑(eval x) F = if x ∈ S then 1 else 0
[PROOFSTEP]
calc
  eval x F = ∏ i in s, eval x (1 - f i ^ (q - 1)) := eval_prod s _ x
  _ = if x ∈ S then 1 else 0 := ?_
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
x : σ → K
⊢ ∏ i in s, ↑(eval x) (1 - f i ^ (q - 1)) = if x ∈ S then 1 else 0
[PROOFSTEP]
simp only [(eval x).map_sub, (eval x).map_pow, (eval x).map_one]
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
x : σ → K
⊢ ∏ x_1 in s, (1 - ↑(eval x) (f x_1) ^ (q - 1)) =
    if x ∈ Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0} then 1 else 0
[PROOFSTEP]
split_ifs with hx
[GOAL]
case pos
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
x : σ → K
hx : x ∈ Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
⊢ ∏ x_1 in s, (1 - ↑(eval x) (f x_1) ^ (q - 1)) = 1
[PROOFSTEP]
apply Finset.prod_eq_one
[GOAL]
case pos.h
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
x : σ → K
hx : x ∈ Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
⊢ ∀ (x_1 : ι), x_1 ∈ s → 1 - ↑(eval x) (f x_1) ^ (q - 1) = 1
[PROOFSTEP]
intro i hi
[GOAL]
case pos.h
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
x : σ → K
hx : x ∈ Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
i : ι
hi : i ∈ s
⊢ 1 - ↑(eval x) (f i) ^ (q - 1) = 1
[PROOFSTEP]
rw [hS] at hx 
[GOAL]
case pos.h
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
x : σ → K
hx : ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
i : ι
hi : i ∈ s
⊢ 1 - ↑(eval x) (f i) ^ (q - 1) = 1
[PROOFSTEP]
rw [hx i hi, zero_pow hq, sub_zero]
[GOAL]
case neg
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
x : σ → K
hx : ¬x ∈ Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
⊢ ∏ x_1 in s, (1 - ↑(eval x) (f x_1) ^ (q - 1)) = 0
[PROOFSTEP]
obtain ⟨i, hi, hx⟩ : ∃ i : ι, i ∈ s ∧ eval x (f i) ≠ 0 := by simpa only [hS, not_forall, not_imp] using hx
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
x : σ → K
hx : ¬x ∈ Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
⊢ ∃ i, i ∈ s ∧ ↑(eval x) (f i) ≠ 0
[PROOFSTEP]
simpa only [hS, not_forall, not_imp] using hx
[GOAL]
case neg.intro.intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
x : σ → K
hx✝ : ¬x ∈ Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
i : ι
hi : i ∈ s
hx : ↑(eval x) (f i) ≠ 0
⊢ ∏ x_1 in s, (1 - ↑(eval x) (f x_1) ^ (q - 1)) = 0
[PROOFSTEP]
apply Finset.prod_eq_zero hi
[GOAL]
case neg.intro.intro
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
x : σ → K
hx✝ : ¬x ∈ Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
i : ι
hi : i ∈ s
hx : ↑(eval x) (f i) ≠ 0
⊢ 1 - ↑(eval x) (f i) ^ (q - 1) = 0
[PROOFSTEP]
rw [pow_card_sub_one_eq_one (eval x (f i)) hx, sub_self]
  -- In particular, we can now show:
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
⊢ p ∣ Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 }
[PROOFSTEP]
have key : ∑ x, eval x F = Fintype.card { x : σ → K // ∀ i ∈ s, eval x (f i) = 0 }
[GOAL]
case key
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
⊢ ∑ x : σ → K, ↑(eval x) F = ↑(Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 })
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
key : ∑ x : σ → K, ↑(eval x) F = ↑(Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 })
⊢ p ∣ Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 }
[PROOFSTEP]
rw [Fintype.card_of_subtype S hS, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one, ← Fintype.sum_extend_by_zero S,
  sum_congr rfl fun x _ => hF x]
  -- With these preparations under our belt, we will approach the main goal.
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
key : ∑ x : σ → K, ↑(eval x) F = ↑(Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 })
⊢ p ∣ Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 }
[PROOFSTEP]
show p ∣ Fintype.card { x // ∀ i : ι, i ∈ s → eval x (f i) = 0 }
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
key : ∑ x : σ → K, ↑(eval x) F = ↑(Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 })
⊢ p ∣ Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 }
[PROOFSTEP]
rw [← CharP.cast_eq_zero_iff K, ← key]
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
key : ∑ x : σ → K, ↑(eval x) F = ↑(Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 })
⊢ ∑ x : σ → K, ↑(eval x) F = 0
[PROOFSTEP]
show
  (∑ x, eval x F) =
    0
      -- We are now ready to apply the main machine, proven before.
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
key : ∑ x : σ → K, ↑(eval x) F = ↑(Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 })
⊢ ∑ x : σ → K, ↑(eval x) F = 0
[PROOFSTEP]
apply F.sum_eval_eq_zero
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
key : ∑ x : σ → K, ↑(eval x) F = ↑(Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 })
⊢ totalDegree F < (q - 1) * Fintype.card σ
[PROOFSTEP]
show F.totalDegree < (q - 1) * Fintype.card σ
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
key : ∑ x : σ → K, ↑(eval x) F = ↑(Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 })
⊢ totalDegree F < (q - 1) * Fintype.card σ
[PROOFSTEP]
calc
  F.totalDegree ≤ ∑ i in s, (1 - f i ^ (q - 1)).totalDegree := totalDegree_finset_prod s _
  _ ≤ ∑ i in s, (q - 1) * (f i).totalDegree :=
    (sum_le_sum fun i _ => ?_)
      -- see ↓
  _ = (q - 1) * ∑ i in s, (f i).totalDegree := mul_sum.symm
  _ < (q - 1) * Fintype.card σ := by
    rwa [mul_lt_mul_left hq]
      -- Now we prove the remaining step from the preceding calculation
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
key : ∑ x : σ → K, ↑(eval x) F = ↑(Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 })
⊢ (q - 1) * ∑ i in s, totalDegree (f i) < (q - 1) * Fintype.card σ
[PROOFSTEP]
rwa [mul_lt_mul_left hq]
  -- Now we prove the remaining step from the preceding calculation
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
key : ∑ x : σ → K, ↑(eval x) F = ↑(Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 })
i : ι
x✝ : i ∈ s
⊢ totalDegree (1 - f i ^ (q - 1)) ≤ (q - 1) * totalDegree (f i)
[PROOFSTEP]
show (1 - f i ^ (q - 1)).totalDegree ≤ (q - 1) * (f i).totalDegree
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
key : ∑ x : σ → K, ↑(eval x) F = ↑(Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 })
i : ι
x✝ : i ∈ s
⊢ totalDegree (1 - f i ^ (q - 1)) ≤ (q - 1) * totalDegree (f i)
[PROOFSTEP]
calc
  (1 - f i ^ (q - 1)).totalDegree ≤ max (1 : MvPolynomial σ K).totalDegree (f i ^ (q - 1)).totalDegree :=
    totalDegree_sub _ _
  _ ≤ (f i ^ (q - 1)).totalDegree := by simp
  _ ≤ (q - 1) * (f i).totalDegree := totalDegree_pow _ _
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i in s, totalDegree (f i) < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := Set.toFinset {x | x ∈ univ ∧ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), ↑(eval x) F = if x ∈ S then 1 else 0
key : ∑ x : σ → K, ↑(eval x) F = ↑(Fintype.card { x // ∀ (i : ι), i ∈ s → ↑(eval x) (f i) = 0 })
i : ι
x✝ : i ∈ s
⊢ max (totalDegree 1) (totalDegree (f i ^ (q - 1))) ≤ totalDegree (f i ^ (q - 1))
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : Fintype K
inst✝⁵ : Field K
inst✝⁴ : Fintype σ
inst✝³ : DecidableEq σ
inst✝² : DecidableEq K
p : ℕ
inst✝¹ : CharP K p
inst✝ : Fintype ι
f : ι → MvPolynomial σ K
h : ∑ i : ι, totalDegree (f i) < Fintype.card σ
⊢ p ∣ Fintype.card { x // ∀ (i : ι), ↑(eval x) (f i) = 0 }
[PROOFSTEP]
simpa using char_dvd_card_solutions_of_sum_lt p h
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : totalDegree f < Fintype.card σ
⊢ p ∣ Fintype.card { x // ↑(eval x) f = 0 }
[PROOFSTEP]
let F : Unit → MvPolynomial σ K := fun _ => f
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : totalDegree f < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
⊢ p ∣ Fintype.card { x // ↑(eval x) f = 0 }
[PROOFSTEP]
have : (∑ i : Unit, (F i).totalDegree) < Fintype.card σ := h
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : totalDegree f < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
this : ∑ i : Unit, totalDegree (F i) < Fintype.card σ
⊢ p ∣ Fintype.card { x // ↑(eval x) f = 0 }
[PROOFSTEP]
convert char_dvd_card_solutions_of_sum_lt p this
[GOAL]
case h.e'_4.h.h.e'_2.h.a
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : totalDegree f < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
this : ∑ i : Unit, totalDegree (F i) < Fintype.card σ
x✝ : σ → K
⊢ ↑(eval x✝) f = 0 ↔ ∀ (i : Unit), i ∈ univ → ↑(eval x✝) (F i) = 0
[PROOFSTEP]
aesop
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : totalDegree f₁ + totalDegree f₂ < Fintype.card σ
⊢ p ∣ Fintype.card { x // ↑(eval x) f₁ = 0 ∧ ↑(eval x) f₂ = 0 }
[PROOFSTEP]
let F : Bool → MvPolynomial σ K := fun b => cond b f₂ f₁
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : totalDegree f₁ + totalDegree f₂ < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b => bif b then f₂ else f₁
⊢ p ∣ Fintype.card { x // ↑(eval x) f₁ = 0 ∧ ↑(eval x) f₂ = 0 }
[PROOFSTEP]
have : (∑ b : Bool, (F b).totalDegree) < Fintype.card σ := (add_comm _ _).trans_lt h
[GOAL]
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : totalDegree f₁ + totalDegree f₂ < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b => bif b then f₂ else f₁
this : ∑ b : Bool, totalDegree (F b) < Fintype.card σ
⊢ p ∣ Fintype.card { x // ↑(eval x) f₁ = 0 ∧ ↑(eval x) f₂ = 0 }
[PROOFSTEP]
simpa only [Bool.forall_bool] using char_dvd_card_solutions_of_fintype_sum_lt p this
