[GOAL]
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
⊢ RingHom.comp (frobenius R p) ↑(RingEquiv.symm (frobeniusEquiv R p)) = RingHom.id R
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x✝ : R
⊢ ↑(RingHom.comp (frobenius R p) ↑(RingEquiv.symm (frobeniusEquiv R p))) x✝ = ↑(RingHom.id R) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
⊢ RingHom.comp (↑(RingEquiv.symm (frobeniusEquiv R p))) (frobenius R p) = RingHom.id R
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x✝ : R
⊢ ↑(RingHom.comp (↑(RingEquiv.symm (frobeniusEquiv R p))) (frobenius R p)) x✝ = ↑(RingHom.id R) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
⊢ ↑(expand R p) f = map (↑(RingEquiv.symm (frobeniusEquiv R p))) f ^ p
[PROOFSTEP]
rw [← (f.map (S := R) (frobeniusEquiv R p).symm).expand_char p, map_expand, map_map, frobenius_comp_frobeniusEquiv_symm,
  map_id]
[GOAL]
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
⊢ ¬Irreducible (↑(expand R p) f)
[PROOFSTEP]
have hp : Fact p.Prime := inferInstance
[GOAL]
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
hp : Fact (Nat.Prime p)
⊢ ¬Irreducible (↑(expand R p) f)
[PROOFSTEP]
rw [polynomial_expand_eq]
[GOAL]
R : Type u_1
p : ℕ
inst✝³ : CommSemiring R
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : R[X]
hp : Fact (Nat.Prime p)
⊢ ¬Irreducible (map (↑(RingEquiv.symm (frobeniusEquiv R p))) f ^ p)
[PROOFSTEP]
exact fun hf ↦ hf.not_unit $ (of_irreducible_pow hp.out.ne_one hf).pow p
[GOAL]
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
⊢ PerfectRing (R × S) p
[PROOFSTEP]
constructor
[GOAL]
case bijective_frobenius
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
⊢ Bijective ↑(frobenius (R × S) p)
[PROOFSTEP]
have : frobenius (R × S) p = Prod.map (frobenius R p) (frobenius S p) := by ext <;> simp [frobenius_def]
[GOAL]
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
⊢ ↑(frobenius (R × S) p) = Prod.map ↑(frobenius R p) ↑(frobenius S p)
[PROOFSTEP]
ext
[GOAL]
case h.h₁
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
x✝ : R × S
⊢ (↑(frobenius (R × S) p) x✝).fst = (Prod.map (↑(frobenius R p)) (↑(frobenius S p)) x✝).fst
[PROOFSTEP]
simp [frobenius_def]
[GOAL]
case h.h₂
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
x✝ : R × S
⊢ (↑(frobenius (R × S) p) x✝).snd = (Prod.map (↑(frobenius R p)) (↑(frobenius S p)) x✝).snd
[PROOFSTEP]
simp [frobenius_def]
[GOAL]
case bijective_frobenius
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
this : ↑(frobenius (R × S) p) = Prod.map ↑(frobenius R p) ↑(frobenius S p)
⊢ Bijective ↑(frobenius (R × S) p)
[PROOFSTEP]
rw [this]
[GOAL]
case bijective_frobenius
R : Type ?u.337703
p : ℕ
inst✝⁶ : CommSemiring R
inst✝⁵ : Fact (Nat.Prime p)
inst✝⁴ : CharP R p
inst✝³ : PerfectRing R p
S : Type ?u.337974
inst✝² : CommSemiring S
inst✝¹ : CharP S p
inst✝ : PerfectRing S p
this : ↑(frobenius (R × S) p) = Prod.map ↑(frobenius R p) ↑(frobenius S p)
⊢ Bijective (Prod.map ↑(frobenius R p) ↑(frobenius S p))
[PROOFSTEP]
exact Bijective.Prod_map (bijective_frobenius R p) (bijective_frobenius S p)
[GOAL]
K : Type u_1
p : ℕ
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : PerfectRing K p
⊢ PerfectField K
[PROOFSTEP]
refine' PerfectField.mk $ fun hf ↦ _
[GOAL]
K : Type u_1
p : ℕ
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : PerfectRing K p
f✝ : K[X]
hf : Irreducible f✝
⊢ Separable f✝
[PROOFSTEP]
rcases separable_or p hf with h | ⟨-, g, -, rfl⟩
[GOAL]
case inl
K : Type u_1
p : ℕ
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : PerfectRing K p
f✝ : K[X]
hf : Irreducible f✝
h : Separable f✝
⊢ Separable f✝
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.intro.intro
K : Type u_1
p : ℕ
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : PerfectRing K p
g : K[X]
hf : Irreducible (↑(expand K p) g)
⊢ Separable (↑(expand K p) g)
[PROOFSTEP]
exfalso
[GOAL]
case inr.intro.intro.intro.h
K : Type u_1
p : ℕ
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : PerfectRing K p
g : K[X]
hf : Irreducible (↑(expand K p) g)
⊢ False
[PROOFSTEP]
revert hf
[GOAL]
case inr.intro.intro.intro.h
K : Type u_1
p : ℕ
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : PerfectRing K p
g : K[X]
⊢ Irreducible (↑(expand K p) g) → False
[PROOFSTEP]
simp
[GOAL]
K : Type ?u.469717
inst✝¹ : Field K
inst✝ : Finite K
⊢ PerfectField K
[PROOFSTEP]
obtain ⟨p, _instP⟩ := CharP.exists K
[GOAL]
case intro
K : Type ?u.469717
inst✝¹ : Field K
inst✝ : Finite K
p : ℕ
_instP : CharP K p
⊢ PerfectField K
[PROOFSTEP]
have : Fact p.Prime := ⟨CharP.char_is_prime K p⟩
[GOAL]
case intro
K : Type ?u.469717
inst✝¹ : Field K
inst✝ : Finite K
p : ℕ
_instP : CharP K p
this : Fact (Nat.Prime p)
⊢ PerfectField K
[PROOFSTEP]
exact PerfectRing.toPerfectField K p
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ PerfectRing K p
[PROOFSTEP]
refine' PerfectRing.ofSurjective _ _ $ fun y ↦ _
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
let f : K[X] := X ^ p - C y
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
let L := f.SplittingField
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
let ι := algebraMap K L
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
have hf_deg : f.degree ≠ 0 := by rw [degree_X_pow_sub_C hp.out.pos y, p.cast_ne_zero]; exact hp.out.ne_zero
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
⊢ degree f ≠ 0
[PROOFSTEP]
rw [degree_X_pow_sub_C hp.out.pos y, p.cast_ne_zero]
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
⊢ p ≠ 0
[PROOFSTEP]
exact hp.out.ne_zero
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
let a : L := f.rootOfSplits ι (SplittingField.splits f) hf_deg
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
have hfa : aeval a f = 0 := by rw [aeval_def, map_rootOfSplits _ (SplittingField.splits f) hf_deg]
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
⊢ ↑(aeval a) f = 0
[PROOFSTEP]
rw [aeval_def, map_rootOfSplits _ (SplittingField.splits f) hf_deg]
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
have ha_pow : a ^ p = ι y := by rwa [AlgHom.map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hfa
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
⊢ a ^ p = ↑ι y
[PROOFSTEP]
rwa [AlgHom.map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hfa
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
let g : K[X] := minpoly K a
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
suffices : (g.map ι).natDegree = 1
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
this : natDegree (map ι g) = 1
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
rw [g.natDegree_map, ← degree_eq_iff_natDegree_eq_of_pos Nat.one_pos] at this
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
this : degree g = ↑1
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
obtain ⟨a' : K, ha' : ι a' = a⟩ := minpoly.mem_range_of_degree_eq_one K a this
[GOAL]
case intro
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
this : degree g = ↑1
a' : K
ha' : ↑ι a' = a
⊢ ∃ a, ↑(frobenius K p) a = y
[PROOFSTEP]
refine' ⟨a', NoZeroSMulDivisors.algebraMap_injective K L _⟩
[GOAL]
case intro
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
this : degree g = ↑1
a' : K
ha' : ↑ι a' = a
⊢ ↑(algebraMap K L) (↑(frobenius K p) a') = ↑(algebraMap K L) y
[PROOFSTEP]
rw [RingHom.map_frobenius, ha', frobenius_def, ha_pow]
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
⊢ natDegree (map ι g) = 1
[PROOFSTEP]
have hg_dvd : g.map ι ∣ (X - C a) ^ p :=
  by
  convert Polynomial.map_dvd ι (minpoly.dvd K a hfa)
  rw [sub_pow_char, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, ← ha_pow, map_pow]
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
⊢ map ι g ∣ (X - ↑C a) ^ p
[PROOFSTEP]
convert Polynomial.map_dvd ι (minpoly.dvd K a hfa)
[GOAL]
case h.e'_4
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
⊢ (X - ↑C a) ^ p = map ι f
[PROOFSTEP]
rw [sub_pow_char, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, ← ha_pow, map_pow]
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
⊢ natDegree (map ι g) = 1
[PROOFSTEP]
have ha : IsIntegral K a := isIntegral_of_finite K a
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
⊢ natDegree (map ι g) = 1
[PROOFSTEP]
have hg_pow : g.map ι = (X - C a) ^ (g.map ι).natDegree :=
  by
  obtain ⟨q, -, hq⟩ := (dvd_prime_pow (prime_X_sub_C a) p).mp hg_dvd
  rw [eq_of_monic_of_associated ((minpoly.monic ha).map ι) ((monic_X_sub_C a).pow q) hq, natDegree_pow,
    natDegree_X_sub_C, mul_one]
[GOAL]
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
⊢ map ι g = (X - ↑C a) ^ natDegree (map ι g)
[PROOFSTEP]
obtain ⟨q, -, hq⟩ := (dvd_prime_pow (prime_X_sub_C a) p).mp hg_dvd
[GOAL]
case intro.intro
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
q : ℕ
hq : Associated (map ι g) ((X - ↑C a) ^ q)
⊢ map ι g = (X - ↑C a) ^ natDegree (map ι g)
[PROOFSTEP]
rw [eq_of_monic_of_associated ((minpoly.monic ha).map ι) ((monic_X_sub_C a).pow q) hq, natDegree_pow, natDegree_X_sub_C,
  mul_one]
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
hg_pow : map ι g = (X - ↑C a) ^ natDegree (map ι g)
⊢ natDegree (map ι g) = 1
[PROOFSTEP]
have hg_sep : (g.map ι).Separable := (separable_of_irreducible $ minpoly.irreducible ha).map
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
hg_pow : map ι g = (X - ↑C a) ^ natDegree (map ι g)
hg_sep : Separable (map ι g)
⊢ natDegree (map ι g) = 1
[PROOFSTEP]
rw [hg_pow] at hg_sep
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
hg_pow : map ι g = (X - ↑C a) ^ natDegree (map ι g)
hg_sep : Separable ((X - ↑C a) ^ natDegree (map ι g))
⊢ natDegree (map ι g) = 1
[PROOFSTEP]
refine' (Separable.of_pow (not_isUnit_X_sub_C a) _ hg_sep).2
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
hg_pow : map ι g = (X - ↑C a) ^ natDegree (map ι g)
hg_sep : Separable ((X - ↑C a) ^ natDegree (map ι g))
⊢ natDegree (map ι g) ≠ 0
[PROOFSTEP]
rw [g.natDegree_map ι, ← Nat.pos_iff_ne_zero, natDegree_pos_iff_degree_pos]
[GOAL]
case this
K : Type ?u.470721
inst✝² : Field K
inst✝¹ : PerfectField K
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP K p
y : K
f : K[X] := X ^ p - ↑C y
L : Type ?u.470721 := SplittingField f
ι : K →+* L := algebraMap K L
hf_deg : degree f ≠ 0
a : L := rootOfSplits ι (_ : Splits (algebraMap K (SplittingField f)) f) hf_deg
hfa : ↑(aeval a) f = 0
ha_pow : a ^ p = ↑ι y
g : K[X] := minpoly K a
hg_dvd : map ι g ∣ (X - ↑C a) ^ p
ha : IsIntegral K a
hg_pow : map ι g = (X - ↑C a) ^ natDegree (map ι g)
hg_sep : Separable ((X - ↑C a) ^ natDegree (map ι g))
⊢ 0 < degree g
[PROOFSTEP]
exact minpoly.degree_pos ha


[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
⊢ ∃ b, ↑(Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
[PROOFSTEP]
haveI : Fact (ringChar F).Prime := ⟨CharP.char_is_prime F _⟩
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
⊢ ∃ b, ↑(Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
[PROOFSTEP]
have htr := traceForm_nondegenerate (ZMod (ringChar F)) F a
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (n : F), BilinForm.bilin (Algebra.traceForm (ZMod (ringChar F)) F) a n = 0) → a = 0
⊢ ∃ b, ↑(Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
[PROOFSTEP]
simp_rw [Algebra.traceForm_apply] at htr
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (n : F), ↑(Algebra.trace (ZMod (ringChar F)) F) (a * n) = 0) → a = 0
⊢ ∃ b, ↑(Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
[PROOFSTEP]
by_contra' hf
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (n : F), ↑(Algebra.trace (ZMod (ringChar F)) F) (a * n) = 0) → a = 0
hf : ∀ (b : F), ↑(Algebra.trace (ZMod (ringChar F)) F) (a * b) = 0
⊢ False
[PROOFSTEP]
exact ha (htr hf)


[GOAL]
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots p))))
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
[PROOFSTEP]
rw [← Multiset.prod_toList, AlgHom.map_list_prod] at h
[GOAL]
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit (List.prod (List.map (↑(aeval a)) (Multiset.toList (Multiset.map (fun x => X - ↑C x) (roots p)))))
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
[PROOFSTEP]
replace h := mt List.prod_isUnit h
[GOAL]
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h :
  ¬∀ (m : (fun x => A) (List.prod (Multiset.toList (Multiset.map (fun x => X - ↑C x) (roots p))))),
      m ∈ List.map (↑(aeval a)) (Multiset.toList (Multiset.map (fun x => X - ↑C x) (roots p))) → IsUnit m
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
[PROOFSTEP]
simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map, aeval_X, exists_exists_and_eq_and,
  Multiset.mem_map, AlgHom.map_sub] at h
[GOAL]
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ∃ a_1, a_1 ∈ roots p ∧ ¬IsUnit (a - ↑↑ₐ a_1)
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
[PROOFSTEP]
rcases h with ⟨r, r_mem, r_nu⟩
[GOAL]
case intro.intro
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ roots p
r_nu : ¬IsUnit (a - ↑↑ₐ r)
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
[PROOFSTEP]
exact ⟨r, by rwa [mem_iff, ← IsUnit.sub_iff], (mem_roots'.1 r_mem).2⟩
[GOAL]
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ roots p
r_nu : ¬IsUnit (a - ↑↑ₐ r)
⊢ r ∈ σ a
[PROOFSTEP]
rwa [mem_iff, ← IsUnit.sub_iff]
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
⊢ (fun x => eval x p) '' σ a ⊆ σ (↑(aeval a) p)
[PROOFSTEP]
rintro _ ⟨k, hk, rfl⟩
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
[PROOFSTEP]
let q := C (eval k p) - p
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
[PROOFSTEP]
have hroot : IsRoot q k := by simp only [eval_C, eval_sub, sub_self, IsRoot.def]
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
⊢ IsRoot q k
[PROOFSTEP]
simp only [eval_C, eval_sub, sub_self, IsRoot.def]
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot : IsRoot q k
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
[PROOFSTEP]
rw [← mul_div_eq_iff_isRoot, ← neg_mul_neg, neg_sub] at hroot
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
[PROOFSTEP]
have aeval_q_eq : ↑ₐ (eval k p) - aeval a p = aeval a q := by simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
⊢ ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
[PROOFSTEP]
simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
[PROOFSTEP]
rw [mem_iff, aeval_q_eq, ← hroot, aeval_mul]
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
⊢ ¬IsUnit (↑(aeval a) (↑C k - X) * ↑(aeval a) (-(q / (X - ↑C k))))
[PROOFSTEP]
have hcomm := (Commute.all (C k - X) (-(q / (X - C k)))).map (aeval a : 𝕜[X] →ₐ[𝕜] A)
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
hcomm : Commute (↑(aeval a) (↑C k - X)) (↑(aeval a) (-(q / (X - ↑C k))))
⊢ ¬IsUnit (↑(aeval a) (↑C k - X) * ↑(aeval a) (-(q / (X - ↑C k))))
[PROOFSTEP]
apply mt fun h => (hcomm.isUnit_mul_iff.mp h).1
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
hcomm : Commute (↑(aeval a) (↑C k - X)) (↑(aeval a) (-(q / (X - ↑C k))))
⊢ ¬IsUnit (↑(aeval a) (↑C k - X))
[PROOFSTEP]
simpa only [aeval_X, aeval_C, AlgHom.map_sub] using hk
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
⊢ σ (↑(aeval a) p) = (fun x => eval x p) '' σ a
[PROOFSTEP]
refine'
  Set.eq_of_subset_of_subset (fun k hk => _)
    (subset_polynomial_aeval a p)
      -- write `C k - p` product of linear factors and a constant; show `C k - p ≠ 0`.
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
have hprod := eq_prod_roots_of_splits_id (IsAlgClosed.splits (C k - p))
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
have h_ne : C k - p ≠ 0 :=
  ne_zero_of_degree_gt <| by rwa [degree_sub_eq_right_of_degree_lt (lt_of_le_of_lt degree_C_le hdeg)]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
⊢ ?m.286583 < degree (↑C k - p)
[PROOFSTEP]
rwa [degree_sub_eq_right_of_degree_lt (lt_of_le_of_lt degree_C_le hdeg)]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
have lead_ne := leadingCoeff_ne_zero.mpr h_ne
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
have lead_unit := (Units.map ↑ₐ.toMonoidHom (Units.mk0 _ lead_ne)).isUnit
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
have p_a_eq : aeval a (C k - p) = ↑ₐ k - aeval a p := by simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
⊢ ↑(aeval a) (↑C k - p) = ↑↑ₐ k - ↑(aeval a) p
[PROOFSTEP]
simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
p_a_eq : ↑(aeval a) (↑C k - p) = ↑↑ₐ k - ↑(aeval a) p
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
rw [mem_iff, ← p_a_eq, hprod, aeval_mul, ((Commute.all _ _).map (aeval a : 𝕜[X] →ₐ[𝕜] A)).isUnit_mul_iff, aeval_C] at hk
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk :
  ¬(IsUnit (↑↑ₐ (leadingCoeff (↑C k - p))) ∧
      IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p))))))
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
p_a_eq : ↑(aeval a) (↑C k - p) = ↑↑ₐ k - ↑(aeval a) p
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
replace hk := exists_mem_of_not_isUnit_aeval_prod (not_and.mp hk lead_unit)
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
p_a_eq : ↑(aeval a) (↑C k - p) = ↑↑ₐ k - ↑(aeval a) p
hk : ∃ k_1, k_1 ∈ σ a ∧ eval k_1 (↑C k - p) = 0
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
rcases hk with ⟨r, r_mem, r_ev⟩
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
p_a_eq : ↑(aeval a) (↑C k - p) = ↑↑ₐ k - ↑(aeval a) p
r : 𝕜
r_mem : r ∈ σ a
r_ev : eval r (↑C k - p) = 0
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
exact ⟨r, r_mem, symm (by simpa [eval_sub, eval_C, sub_eq_zero] using r_ev)⟩
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
p_a_eq : ↑(aeval a) (↑C k - p) = ↑↑ₐ k - ↑(aeval a) p
r : 𝕜
r_mem : r ∈ σ a
r_ev : eval r (↑C k - p) = 0
⊢ k = (fun x => eval x p) r
[PROOFSTEP]
simpa [eval_sub, eval_C, sub_eq_zero] using r_ev
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
⊢ σ (↑(aeval a) p) = (fun k => eval k p) '' σ a
[PROOFSTEP]
nontriviality A
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
✝ : Nontrivial A
⊢ σ (↑(aeval a) p) = (fun k => eval k p) '' σ a
[PROOFSTEP]
refine' Or.elim (le_or_gt (degree p) 0) (fun h => _) (map_polynomial_aeval_of_degree_pos a p)
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
✝ : Nontrivial A
h : degree p ≤ 0
⊢ σ (↑(aeval a) p) = (fun k => eval k p) '' σ a
[PROOFSTEP]
rw [eq_C_of_degree_le_zero h]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
✝ : Nontrivial A
h : degree p ≤ 0
⊢ σ (↑(aeval a) (↑C (coeff p 0))) = (fun k => eval k (↑C (coeff p 0))) '' σ a
[PROOFSTEP]
simp only [Set.image_congr, eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon]
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
n : ℕ
⊢ (fun x => x ^ n) '' σ a ⊆ σ (a ^ n)
[PROOFSTEP]
simpa only [eval_pow, eval_X, aeval_X_pow] using subset_polynomial_aeval a (X ^ n : 𝕜[X])
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
n : ℕ
hn : 0 < n
⊢ σ (a ^ n) = (fun x => x ^ n) '' σ a
[PROOFSTEP]
simpa only [aeval_X_pow, eval_pow, eval_X] using
  map_polynomial_aeval_of_degree_pos a (X ^ n : 𝕜[X]) (by rwa [degree_X_pow, Nat.cast_pos])
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
n : ℕ
hn : 0 < n
⊢ 0 < degree (X ^ n)
[PROOFSTEP]
rwa [degree_X_pow, Nat.cast_pos]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
ha : Set.Nonempty (σ a)
n : ℕ
⊢ σ (a ^ n) = (fun x => x ^ n) '' σ a
[PROOFSTEP]
simpa only [aeval_X_pow, eval_pow, eval_X] using map_polynomial_aeval_of_nonempty a (X ^ n) ha
[GOAL]
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
⊢ Set.Nonempty (σ a)
[PROOFSTEP]
obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 I) a
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
⊢ Set.Nonempty (σ a)
[PROOFSTEP]
have nu : ¬IsUnit (aeval a p) := by rw [← aeval_def] at h_eval_p ; rw [h_eval_p]; simp
[GOAL]
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
⊢ ¬IsUnit (↑(aeval a) p)
[PROOFSTEP]
rw [← aeval_def] at h_eval_p
[GOAL]
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : ↑(aeval a) p = 0
⊢ ¬IsUnit (↑(aeval a) p)
[PROOFSTEP]
rw [h_eval_p]
[GOAL]
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : ↑(aeval a) p = 0
⊢ ¬IsUnit 0
[PROOFSTEP]
simp
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit (↑(aeval a) p)
⊢ Set.Nonempty (σ a)
[PROOFSTEP]
rw [eq_prod_roots_of_monic_of_splits_id h_mon (IsAlgClosed.splits p)] at nu
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))))
⊢ Set.Nonempty (σ a)
[PROOFSTEP]
obtain ⟨k, hk, _⟩ := exists_mem_of_not_isUnit_aeval_prod nu
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))))
k : 𝕜
hk : k ∈ σ a
right✝ : eval k p = 0
⊢ Set.Nonempty (σ a)
[PROOFSTEP]
exact ⟨k, hk⟩


[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