awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
x₀ : { j : σ // j ≠ i } → K
e : K ≃ { x : σ → K // x ∘ Subtype.val (p := fun (j : σ) ↦ j ≠ i) = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
rw : HMul.hMul (α := K) (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)) 0 = 0
⊢ HMul.hMul (α := K) (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ))
      (∑ a : K, HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ)) =
    0
have rw₁ : Eq.{u_1 + 1} (α := K) 0 0
Tactic: rw [sum_pow_lt_card_sub_one K _ hi, mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
x₀ : { j : σ // j ≠ i } → K
e : K ≃ { x : σ → K // x ∘ Subtype.val (p := fun (j : σ) ↦ j ≠ i) = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ Eq.{u_1 + 1} (α := K)
    (∑ x : { x : σ → K // x ∘ Subtype.val = x₀ },
      ∏ j : σ, HPow.hPow (β := ℕ) ((↑x : σ → K) j) ((d : (a : σ) → ℕ) j : ℕ))
    0
have x : ∀ (a : K),
  ∏ j : σ,
      HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) j)
        ((d : (a : σ) → ℕ) j : ℕ) =
    (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)) *
      HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ)
Tactic: 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]
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this_1 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
x₀ : { j : σ // j ≠ i } → K
e : K ≃ { x : σ → K // x ∘ Subtype.val (p := fun (j : σ) ↦ j ≠ i) = 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 } := { default := Subtype.mk (p := fun (j : σ) ↦ j = i) i ⋯, uniq := ⋯ }
⊢ ∏ j : σ,
      HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) j)
        ((d : (a : σ) → ℕ) j : ℕ) =
    HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) i)
        ((d : (a : σ) → ℕ) i : ℕ) *
      ∏ j : { j : σ // j ≠ i },
        HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) (↑j : σ))
          ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)
have rw : HPow.hPow (α := K) (β := ℕ)
      ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K)
        ((e' : (a : { j : σ // j = i } ⊕ { j : σ // j ≠ i }) → σ) (Sum.inl default)))
      ((d : (a : σ) → ℕ) ((e' : (a : { j : σ // j = i } ⊕ { j : σ // j ≠ i }) → σ) (Sum.inl default) : σ) : ℕ) *
    ∏ a₂ : { j : σ // j ≠ i },
      HPow.hPow (α := K) (β := ℕ)
        ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K)
          ((e' : (a : { j : σ // j = i } ⊕ { j : σ // j ≠ i }) → σ) (Sum.inr a₂)))
        ((d : (a : σ) → ℕ) ((e' : (a : { j : σ // j = i } ⊕ { j : σ // j ≠ i }) → σ) (Sum.inr a₂) : σ) : ℕ) =
  HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) i)
      ((d : (a : σ) → ℕ) i : ℕ) *
    ∏ j : { j : σ // j ≠ i },
      HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) (↑j : σ))
        ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)
Tactic: rw [← e'.prod_comp, Fintype.prod_sum_type, univ_unique, prod_singleton]
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this_1 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
x₀ : { j : σ // j ≠ i } → K
e : K ≃ { x : σ → K // x ∘ Subtype.val (p := fun (j : σ) ↦ j ≠ i) = 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 } := { default := Subtype.mk (p := fun (j : σ) ↦ j = i) i ⋯, uniq := ⋯ }
⊢ HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) i)
        ((d : (a : σ) → ℕ) i : ℕ) *
      ∏ j : { j : σ // j ≠ i },
        HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) (↑j : σ))
          ((d : (a : σ) → ℕ) (↑j : σ) : ℕ) =
    HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ) *
      ∏ j : { j : σ // j ≠ i },
        HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) (↑j : σ))
          ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)
have rw : HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ) *
    ∏ j : { j : σ // j ≠ i },
      HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) (↑j : σ))
        ((d : (a : σ) → ℕ) (↑j : σ) : ℕ) =
  HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ) *
    ∏ j : { j : σ // j ≠ i },
      HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) (↑j : σ))
        ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)
Tactic: rw [Equiv.subtypeEquivCodomain_symm_apply_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this_1 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
x₀ : { j : σ // j ≠ i } → K
e : K ≃ { x : σ → K // x ∘ Subtype.val (p := fun (j : σ) ↦ j ≠ i) = 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 } := { default := Subtype.mk (p := fun (j : σ) ↦ j = i) i ⋯, uniq := ⋯ }
⊢ ∏ j : σ,
      HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) j)
        ((d : (a : σ) → ℕ) j : ℕ) =
    (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)) *
      HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ)
have j : ∀ (a_1 : { j : σ // j ≠ i }),
  HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) (↑a_1 : σ))
      ((d : (a : σ) → ℕ) (↑a_1 : σ) : ℕ) =
    HPow.hPow (β := ℕ) (x₀ a_1) ((d : (a : σ) → ℕ) (↑a_1 : σ) : ℕ)
Tactic: 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 _ _
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this_1 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
x₀ : { j : σ // j ≠ i } → K
e : K ≃ { x : σ → K // x ∘ Subtype.val (p := fun (j : σ) ↦ j ≠ i) = 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 } := { default := Subtype.mk (p := fun (j : σ) ↦ j = i) i ⋯, uniq := ⋯ }
j : σ
hj : j ≠ i
⊢ HPow.hPow (α := K) (β := ℕ)
      ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K)
        (↑(Subtype.mk (p := fun (j : σ) ↦ j ≠ i) j hj) : σ))
      ((d : (a : σ) → ℕ) (↑(Subtype.mk (p := fun (j : σ) ↦ j ≠ i) j hj) : σ) : ℕ) =
    HPow.hPow (β := ℕ) (x₀ (Subtype.mk (p := fun (j : σ) ↦ j ≠ i) j hj))
      ((d : (a : σ) → ℕ) (↑(Subtype.mk (p := fun (j : σ) ↦ j ≠ i) j hj) : σ) : ℕ)
have change : HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) j)
    ((d : (a : σ) → ℕ) j : ℕ) =
  HPow.hPow (β := ℕ) (x₀ (Subtype.mk (p := fun (j : σ) ↦ j ≠ i) j hj)) ((d : (a : σ) → ℕ) j : ℕ)
Tactic: change (e a : σ → K) j ^ d j = x₀ ⟨j, hj⟩ ^ d j
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this_1 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
x₀ : { j : σ // j ≠ i } → K
e : K ≃ { x : σ → K // x ∘ Subtype.val (p := fun (j : σ) ↦ j ≠ i) = 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 } := { default := Subtype.mk (p := fun (j : σ) ↦ j = i) i ⋯, uniq := ⋯ }
j : σ
hj : j ≠ i
⊢ HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) j)
      ((d : (a : σ) → ℕ) j : ℕ) =
    HPow.hPow (β := ℕ) (x₀ (Subtype.mk (p := fun (j : σ) ↦ j ≠ i) j hj)) ((d : (a : σ) → ℕ) j : ℕ)
have rw : HPow.hPow (β := ℕ) (x₀ (Subtype.mk (p := fun (x' : σ) ↦ x' ≠ i) j hj)) ((d : (a : σ) → ℕ) j : ℕ) =
  HPow.hPow (β := ℕ) (x₀ (Subtype.mk (p := fun (j : σ) ↦ j ≠ i) j hj)) ((d : (a : σ) → ℕ) j : ℕ)
Tactic: rw [Equiv.subtypeEquivCodomain_symm_apply_ne]
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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 σ
⊢ 0 < q - 1
have rw : Nonempty.{u_1 + 1} Kˣ
Tactic: rw [← Fintype.card_units, Fintype.card_pos_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (hypothesis)
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 σ
⊢ p ∣
    Fintype.card
      { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }
have hq : 0 < q - 1
Tactic: have hq : 0 < q - 1 := by rw [← Fintype.card_units, Fintype.card_pos_iff]; exact ⟨1⟩
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (hypothesis)
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)}
⊢ p ∣
    Fintype.card
      { x : σ → K // ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K) }
have hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
Tactic: have hS (x : σ → K) : x ∈ S ↔ ∀ i ∈ s, eval x (f i) = 0 := by simp [S]
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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)
have eval : Eq.{u_1 + 1} (α := K) (∏ i ∈ s, (eval x : (a : MvPolynomial σ K) → K) (1 - f i ^ (q - 1))) (if x ∈ S then 1 else 0)
Tactic: calc
      eval x F = ∏ i ∈ s, eval x (1 - f i ^ (q - 1)) := eval_prod s _ x
      _ = if x ∈ S then 1 else 0 := ?_
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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) (∏ i ∈ s, (eval x : (a : MvPolynomial σ K) → K) (1 - f i ^ (q - 1))) (if x ∈ S then 1 else 0)
have simp : Eq.{u_1 + 1} (α := K) (∏ x_1 ∈ s, (1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f x_1) : K) (q - 1)))
  (if x ∈ S then 1 else 0)
Tactic: simp only [(eval x).map_sub, (eval x).map_pow, (eval x).map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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)
    (∏ x_1 ∈ s, (1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f x_1) : K) (q - 1)))
    (if x ∈ S then 1 else 0)
have pos : ∀ (hx : x ∈ S),
  Eq.{u_1 + 1} (α := K)
    (∏ x_1 ∈ s, (1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f x_1) : K) (q - 1))) 1
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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
pos :
  ∀ (hx : x ∈ S),
    Eq.{u_1 + 1} (α := K)
      (∏ x_1 ∈ s, (1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f x_1) : K) (q - 1))) 1
⊢ Eq.{u_1 + 1} (α := K)
    (∏ x_1 ∈ s, (1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f x_1) : K) (q - 1)))
    (if x ∈ S then 1 else 0)
have neg : ∀ (hx : x ∉ S),
  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: split_ifs with hx
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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
⊢ Eq.{u_1 + 1} (α := K)
    (∏ x_1 ∈ s, (1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f x_1) : K) (q - 1))) 1
have pos : ∀ x_1 ∈ s, 1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f x_1) : K) (q - 1) = 1
Tactic: apply Finset.prod_eq_one
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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
i : ι
hi : i ∈ s
⊢ 1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (q - 1) = 1
have pos : ∀ (hx : ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)) (i : ι) (hi : i ∈ s),
  1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (q - 1) = 1
Tactic: rw [hS] at hx
Cleared hypotheses: hx, i, hi
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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 : ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
i : ι
hi : i ∈ s
⊢ 1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (q - 1) = 1
have pos : 1 - HPow.hPow (α := K) 0 (q - 1) = 1
Tactic: rw [hx i hi, zero_pow hq.ne', sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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 : ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
i : ι
hi : i ∈ s
pos : 1 - HPow.hPow (α := K) 0 (q - 1) = 1
⊢ 1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (q - 1) = 1
have pos₁ : HSub.hSub (α := K) 1 0 = 1
Tactic: rw [hx i hi, zero_pow hq.ne', sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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 : ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
i : ι
hi : i ∈ s
pos : 1 - HPow.hPow (α := K) 0 (q - 1) = 1
pos₁ : HSub.hSub (α := K) 1 0 = 1
⊢ 1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (q - 1) = 1
have pos₂ : Eq.{u_1 + 1} (α := K) 1 1
Tactic: rw [hx i hi, zero_pow hq.ne', sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨i, hi, hx⟩ : ∃ i ∈ s, eval x (f i) ≠ 0 := by
        simpa [hS, not_forall, Classical.not_imp] using hx
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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)
⊢ 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
have neg : 1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (q - 1) = 0
Tactic: apply Finset.prod_eq_zero hi
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
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)
⊢ 1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (q - 1) = 0
have neg : HSub.hSub (α := K) 1 1 = 0
Tactic: rw [pow_card_sub_one_eq_one (eval x (f i)) hx, sub_self]