awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx : x ∉ S
neg :
  ∀ (i : ι) (hi : i ∈ s) (hx : Ne.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)),
    Eq.{u_1 + 1} (α := K)
      (∏ x_1 ∈ s, (1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f x_1) : K) (q - 1))) 0
⊢ Eq.{u_1 + 1} (α := K)
    (∏ x_1 ∈ s, (1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f x_1) : K) (q - 1))) 0

Tactic:
obtain ⟨i, hi, hx⟩ : ∃ i ∈ s, eval x (f i) ≠ 0 := by
        simpa [hS, not_forall, Classical.not_imp] using hx
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx_1 : x ∉ S
i : ι
hi : i ∈ s
hx : Ne.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
neg : 1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (q - 1) = 0
⊢ Eq.{u_1 + 1} (α := K)
    (∏ x_1 ∈ s, (1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f x_1) : K) (q - 1))) 0

Tactic:
apply Finset.prod_eq_zero hi

Premises used: Finset.prod_eq_zero
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx_1 : x ∉ S
i : ι
hi : i ∈ s
hx : Ne.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
neg : HSub.hSub (α := K) 1 1 = 0
neg₁ neg₂ : Eq.{u_1 + 1} (α := K) 0 0
⊢ 1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (q - 1) = 0

Tactic:
rw [pow_card_sub_one_eq_one (eval x (f i)) hx, sub_self]

Premises used: FiniteField.pow_card_sub_one_eq_one, sub_self, MvPolynomial.eval, DFunLike.coe
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
⊢ ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)

Tactic:
have hF : ∀ x, eval x F = if x ∈ S then 1 else 0 := by
    intro x
    calc
      eval x F = ∏ i ∈ 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.ne', sub_zero]
    · obtain ⟨i, hi, hx⟩ : ∃ i ∈ s, eval x (f i) ≠ 0 := by
        simpa [hS, not_forall, Classical.not_imp] using hx
      apply Finset.prod_eq_zero hi
      rw [pow_card_sub_one_eq_one (eval x (f i)) hx, sub_self]
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
rw : Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F) (↑(#S) : K)
rw₁ : Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F) (↑(∑ x ∈ S, 1) : K)
rw₂ : Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F) (∑ x ∈ S, (↑1 : K))
rw₃ : Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F) (∑ x ∈ S, 1)
rw₄ : Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F) (∑ i : σ → K, if i ∈ S then 1 else 0)
rw₅ rw₆ : Eq.{u_1 + 1} (α := K) (∑ x : σ → K, if x ∈ S then 1 else 0) (∑ i : σ → K, if i ∈ S then 1 else 0)
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)

Tactic:
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]

Premises used: Finset.card_eq_sum_ones, Nat.cast_sum, Fintype.sum_extend_by_zero, Fintype.card_of_subtype, Nat.cast_one, Finset.sum_congr, rfl
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)

Tactic:
have key : ∑ x, eval x F = Fintype.card { x : σ → K // ∀ i ∈ s, eval x (f i) = 0 } := by
    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]
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
change :
  p ∣
    Fintype.card
      { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }
⊢ p ∣
    Fintype.card
      { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }

Tactic:
change p ∣ Fintype.card { x // ∀ i : ι, i ∈ s → eval x (f i) = 0 }

Premises used: Fintype.card, Subtype
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
rw : Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F) 0
⊢ p ∣
    Fintype.card
      { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }

Tactic:
rw [← CharP.cast_eq_zero_iff K, ← key]

Premises used: CharP.cast_eq_zero_iff
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
change : Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F) 0
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F) 0

Tactic:
change (∑ x, eval x F) = 0

Premises used: Finset.univ, MvPolynomial.eval, DFunLike.coe, Finset.sum
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
apply : F.totalDegree < (q - 1) * Fintype.card σ
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F) 0

Tactic:
apply F.sum_eval_eq_zero

Premises used: MvPolynomial.sum_eval_eq_zero
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
⊢ F.totalDegree ≤ ∑ i ∈ s, (1 - f i ^ (q - 1)).totalDegree

Tactic:
totalDegree_finsetProd s _

Premises used: MvPolynomial.totalDegree_finsetProd
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
⊢ LE.le (α := ℕ) (∑ i ∈ s, (1 - f i ^ (q - 1)).totalDegree) (∑ i ∈ s, (q - 1) * (f i).totalDegree)

Tactic:
sum_le_sum fun i _ => ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
⊢ ∑ i ∈ s, (q - 1) * (f i).totalDegree = (q - 1) * ∑ i ∈ s, (f i).totalDegree

Tactic:
(mul_sum ..).symm

Premises used: Finset.mul_sum, Eq.symm
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
ha : 0 < q - 1
⊢ (q - 1) * ∑ i ∈ s, (f i).totalDegree < (q - 1) * Fintype.card σ

Tactic:
gcongr
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
i : ∀ i ∈ s, (1 - f i ^ (q - 1)).totalDegree ≤ (q - 1) * (f i).totalDegree
⊢ F.totalDegree < (q - 1) * Fintype.card σ

Tactic:
calc
    F.totalDegree ≤ ∑ i ∈ s, (1 - f i ^ (q - 1)).totalDegree := totalDegree_finsetProd s _
    _ ≤ ∑ i ∈ s, (q - 1) * (f i).totalDegree := sum_le_sum fun i _ => ?_
    -- see ↓
    _ = (q - 1) * ∑ i ∈ s, (f i).totalDegree := (mul_sum ..).symm
    _ < (q - 1) * Fintype.card σ := by gcongr

Premises used: Finset.mul_sum, Fintype.card, MvPolynomial.totalDegree_finsetProd, MvPolynomial.totalDegree, Finset.sum_le_sum, Eq.symm
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
i : ι
h_1 : i ∈ s
⊢ (1 - f i ^ (q - 1)).totalDegree ≤ max (totalDegree.{u_1, u_2} (R := K) (σ := σ) 1) (f i ^ (q - 1)).totalDegree

Tactic:
totalDegree_sub _ _

Premises used: MvPolynomial.totalDegree_sub
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
i : ι
h_1 : i ∈ s
⊢ max (totalDegree.{u_1, u_2} (R := K) (σ := σ) 1) (f i ^ (q - 1)).totalDegree ≤ (f i ^ (q - 1)).totalDegree

Tactic:
simp
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
i : ι
h_1 : i ∈ s
⊢ (f i ^ (q - 1)).totalDegree ≤ (q - 1) * (f i).totalDegree

Tactic:
totalDegree_pow _ _

Premises used: MvPolynomial.totalDegree_pow
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) :=
  {x : σ → K | ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)
key :
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) F)
    (↑(Fintype.card
          { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }) :
      K)
i : ι
h_1 : i ∈ s
f₁ : max (totalDegree.{u_1, u_2} (R := K) (σ := σ) 1) (f i ^ (q - 1)).totalDegree ≤ (f i ^ (q - 1)).totalDegree
⊢ (1 - f i ^ (q - 1)).totalDegree ≤ (q - 1) * (f i).totalDegree

Tactic:
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 _ _

Premises used: MvPolynomial.totalDegree_pow, MvPolynomial.totalDegree, MvPolynomial.totalDegree_sub
-- Module: Mathlib.FieldTheory.ChevalleyWarning
Goal:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
inst_4 : DecidableEq K
p : ℕ
inst_5 : CharP K p
inst_6 : Fintype ι
f : ι → MvPolynomial σ K
h : ∑ i : ι, (f i).totalDegree < Fintype.card σ
⊢ p ∣
    Fintype.card
      { x : σ → K // ∀ (i : ι), Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }

Tactic:
simpa using char_dvd_card_solutions_of_sum_lt p h

Premises used: char_dvd_card_solutions_of_sum_lt