awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.ChevalleyWarning
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 := ⋯ }
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 : σ) : ℕ)
⊢ ∏ 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 : σ) : ℕ)

Tactic:
rw [← e'.prod_comp, Fintype.prod_sum_type, univ_unique, prod_singleton]

Premises used: Finset.prod_singleton, Finset.univ_unique, Equiv.prod_comp, Fintype.prod_sum_type
-- Module: Mathlib.FieldTheory.ChevalleyWarning
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)
          ((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:
rfl
-- Module: Mathlib.FieldTheory.ChevalleyWarning
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 := ⋯ }
rw 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 : σ) : ℕ)
⊢ 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 : σ) : ℕ)

Tactic:
rw [Equiv.subtypeEquivCodomain_symm_apply_eq]

Premises used: Equiv.subtypeEquivCodomain_symm_apply_eq
-- Module: Mathlib.FieldTheory.ChevalleyWarning
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 (β := ℕ) 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 (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)

Tactic:
congr_arg _ (Fintype.prod_congr _ _ ?_)

Premises used: congr_arg, Fintype.prod_congr
-- Module: Mathlib.FieldTheory.ChevalleyWarning
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 (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ) *
      ∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ) =
    (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)) *
      HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ)

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.FieldTheory.ChevalleyWarning
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 :
  ∀ (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 : σ) : ℕ)
⊢ ∏ 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
    (∏ 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 _ _

Premises used: Finset.univ, Finset.prod, congr_arg, HPow.hPow, mul_comm, Fintype.prod_congr, Subtype.val, DFunLike.coe
-- Module: Mathlib.FieldTheory.ChevalleyWarning
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
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 : ℕ)
⊢ 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) : σ) : ℕ)

Tactic:
change (e a : σ → K) j ^ d j = x₀ ⟨j, hj⟩ ^ d j

Premises used: Subtype.mk, Subtype.val, DFunLike.coe
-- Module: Mathlib.FieldTheory.ChevalleyWarning
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
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 : ℕ)
h₁ : j ≠ i
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 : ℕ)
h₂ : 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 : ℕ)

Tactic:
rw [Equiv.subtypeEquivCodomain_symm_apply_ne]

Premises used: Equiv.subtypeEquivCodomain_symm_apply_ne
-- 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 σ
rw : Nonempty.{u_1 + 1} Kˣ
⊢ 0 < q - 1

Tactic:
rw [← Fintype.card_units, Fintype.card_pos_iff]

Premises used: Fintype.card_units, Fintype.card_pos_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 σ
⊢ Nonempty.{u_1 + 1} Kˣ

Tactic:
⟨1⟩

Premises used: Nonempty.intro, OfNat.ofNat
-- 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 σ
⊢ Nonempty.{u_1 + 1} Kˣ

Tactic:
exact ⟨1⟩
-- 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 σ
⊢ 0 < q - 1

Tactic:
have hq : 0 < q - 1 := by rw [← Fintype.card_units, Fintype.card_pos_iff]; exact ⟨1⟩
-- 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)}
x : σ → K
⊢ x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)

Tactic:
simp [S]
-- 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)}
⊢ ∀ (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]
-- 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)
    (∏ i ∈ s, (eval x : (a : MvPolynomial σ K) → K) (1 - f i ^ (q - 1)) : K)

Tactic:
eval_prod s _ x

Premises used: MvPolynomial.eval_prod
-- 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) (∏ i ∈ s, (eval x : (a : MvPolynomial σ K) → K) (1 - f i ^ (q - 1))) (if x ∈ S then 1 else 0)

Tactic:
?_
-- 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) ((MvPolynomial.eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)}
hS :
  ∀ (x : σ → K),
    x ∈ S ↔ ∀ i ∈ s, Eq.{u_1 + 1} (α := K) ((MvPolynomial.eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
eval :
  Eq.{u_1 + 1} (α := K) (∏ i ∈ s, (MvPolynomial.eval x : (a : MvPolynomial σ K) → K) (1 - f i ^ (q - 1)))
    (if x ∈ S then 1 else 0)
⊢ Eq.{u_1 + 1} (α := K) ((MvPolynomial.eval x : (a : MvPolynomial σ K) → K) F : K) (if x ∈ S then 1 else 0 : K)

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 := ?_

Premises used: MvPolynomial.eval_prod, 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
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)
⊢ 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:
simp only [(eval x).map_sub, (eval x).map_pow, (eval x).map_one]

Premises used: RingHom.map_one, RingHom.map_sub, MvPolynomial.eval, RingHom.map_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))
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
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
⊢ 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:
split_ifs with 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 : x ∈ S
pos : ∀ 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))) 1

Tactic:
apply Finset.prod_eq_one

Premises used: Finset.prod_eq_one
-- 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
i : ι
hi : i ∈ s
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
⊢ 1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (q - 1) = 1

Tactic:
rw [hS] at 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 : ∀ 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
pos₂ pos₃ : Eq.{u_1 + 1} (α := K) 1 1
⊢ 1 - HPow.hPow (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (q - 1) = 1

Tactic:
rw [hx i hi, zero_pow hq.ne', sub_zero]

Premises used: sub_zero, LT.lt.ne', zero_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))
x : σ → K
hx : x ∉ S
⊢ ∃ i ∈ s, Ne.{u_1 + 1} (α := K) ((eval x : (a : MvPolynomial σ K) → K) (f i) : K) (0 : K)

Tactic:
simpa [hS, not_forall, Classical.not_imp] using hx

Premises used: Classical.not_imp, Classical.not_forall