K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
have hq : 0 < q - 1 := by rw [← Fintype.card_units, Fintype.card_pos_iff]; exact ⟨1⟩
K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
let S : Finset (σ → K) := { x ∈ univ | ∀ i ∈ s, eval x (f i) = 0 }.toFinset
K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
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]
K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
let F : MvPolynomial σ K := ∏ i in s, (1 - f i ^ (q - 1))
case key
K : Type u_3
σ : Type u_2
ι : Type u_1
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_3
σ : Type u_2
ι : Type u_1
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 }
K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
have key : (∑ x, eval x F) = Fintype.card { x : σ → K // ∀ i ∈ s, eval x (f i) = 0 }
K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
case key
K : Type u_3
σ : Type u_2
ι : Type u_1
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_3
σ : Type u_2
ι : Type u_1
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 }
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]
K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
show p ∣ Fintype.card { x // ∀ i : ι, i ∈ s → eval x (f i) = 0 }
K : Type u_3
σ : Type u_2
ι : Type u_1
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
K : Type u_3
σ : Type u_2
ι : Type u_1
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 }
rw [← CharP.cast_eq_zero_iff K, ← key]
K : Type u_3
σ : Type u_2
ι : Type u_1
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
K : Type u_3
σ : Type u_2
ι : Type u_1
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
show (∑ x, eval x F) = 0
K : Type u_3
σ : Type u_2
ι : Type u_1
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 σ
K : Type u_3
σ : Type u_2
ι : Type u_1
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
apply F.sum_eval_eq_zero
K : Type u_3
σ : Type u_2
ι : Type u_1
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 σ
K : Type u_3
σ : Type u_2
ι : Type u_1
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 σ
show F.totalDegree < (q - 1) * Fintype.card σ
K : Type u_3
σ : Type u_2
ι : Type u_1
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)
K : Type u_3
σ : Type u_2
ι : Type u_1
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 σ
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 _ => ?_)
  _ = (q - 1) * ∑ i in s, (f i).totalDegree := mul_sum.symm
  _ < (q - 1) * Fintype.card σ := by rwa [mul_lt_mul_left hq]
K : Type u_3
σ : Type u_2
ι : Type u_1
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)
K : Type u_3
σ : Type u_2
ι : Type u_1
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)
show (1 - f i ^ (q - 1)).totalDegree ≤ (q - 1) * (f i).totalDegree
no goals
K : Type u_3
σ : Type u_2
ι : Type u_1
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)
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 _ _
K : Type u_3
σ : Type u_2
ι : Type u_1
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ˣ
K : Type u_3
σ : Type u_2
ι : Type u_1
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
rw [← Fintype.card_units, Fintype.card_pos_iff]
no goals
K : Type u_3
σ : Type u_2
ι : Type u_1
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ˣ
exact ⟨1⟩
K : Type u_3
σ : Type u_2
ι : Type u_1
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
K : Type u_3
σ : Type u_2
ι : Type u_1
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
intro x
no goals
K : Type u_3
σ : Type u_2
ι : Type u_1
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
simp only [Set.toFinset_setOf, mem_univ, true_and, mem_filter]
K : Type u_3
σ : Type u_2
ι : Type u_1
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
K : Type u_3
σ : Type u_2
ι : Type u_1
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
intro x
K : Type u_3
σ : Type u_2
ι : Type u_1
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
K : Type u_3
σ : Type u_2
ι : Type u_1
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
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 := ?_
K : Type u_3
σ : Type u_2
ι : Type u_1
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
K : Type u_3
σ : Type u_2
ι : Type u_1
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
simp only [(eval x).map_sub, (eval x).map_pow, (eval x).map_one]
case inl
K : Type u_3
σ : Type u_2
ι : Type u_1
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

case inr
K : Type u_3
σ : Type u_2
ι : Type u_1
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
K : Type u_3
σ : Type u_2
ι : Type u_1
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
split_ifs with hx
case inl.h
K : Type u_3
σ : Type u_2
ι : Type u_1
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
case inl
K : Type u_3
σ : Type u_2
ι : Type u_1
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
apply Finset.prod_eq_one
case inl.h
K : Type u_3
σ : Type u_2
ι : Type u_1
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
case inl.h
K : Type u_3
σ : Type u_2
ι : Type u_1
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
intro i hi
case inl.h
K : Type u_3
σ : Type u_2
ι : Type u_1
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
case inl.h
K : Type u_3
σ : Type u_2
ι : Type u_1
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
rw [hS] at hx
no goals
case inl.h
K : Type u_3
σ : Type u_2
ι : Type u_1
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
rw [hx i hi, zero_pow hq, sub_zero]
case inr.intro.intro
K : Type u_3
σ : Type u_2
ι : Type u_1
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
case inr
K : Type u_3
σ : Type u_2
ι : Type u_1
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
obtain ⟨i, hi, hx⟩ : ∃ i : ι, i ∈ s ∧ eval x (f i) ≠ 0 := by
  simpa only [hS, not_forall, not_imp] using hx
case inr.intro.intro
K : Type u_3
σ : Type u_2
ι : Type u_1
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
case inr.intro.intro
K : Type u_3
σ : Type u_2
ι : Type u_1
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
apply Finset.prod_eq_zero hi
no goals
case inr.intro.intro
K : Type u_3
σ : Type u_2
ι : Type u_1
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
rw [pow_card_sub_one_eq_one (eval x (f i)) hx, sub_self]
no goals
K : Type u_3
σ : Type u_2
ι : Type u_1
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
simpa only [hS, not_forall, not_imp] using hx
no goals
K : Type u_3
σ : Type u_2
ι : Type u_1
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 σ
rwa [mul_lt_mul_left hq]
no goals
K : Type u_3
σ : Type u_2
ι : Type u_1
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))
simp