awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
a :
  (Cardinal.prod fun (x : (Module.rank F E).ord.ToType) ↦ 2) ≤
    Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))
⊢ HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E) ≤
    Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))

Tactic:
conv_lhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']

Premises used: Cardinal.prod_const', Cardinal.mk_ord_toType, Module.rank
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun (x : (Module.rank F E).ord.ToType) ↦ 2) ≤
    Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))

Tactic:
prod_le_prod _ _ Emb.Cardinal.two_le_deg

Premises used: Field.Emb.Cardinal.two_le_deg, Cardinal.prod_le_prod
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun (x : (Module.rank F E).ord.ToType) ↦ 2) ≤
    Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))

Tactic:
exact prod_le_prod _ _ Emb.Cardinal.two_le_deg

Premises used: Field.Emb.Cardinal.two_le_deg, Cardinal.prod_le_prod
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
pos : ∀ (h : ℵ₀ ≤ Module.rank F E), #(Emb F E) = HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
neg : ∀ (h : ¬ℵ₀ ≤ Module.rank F E), #(Emb F E) = Module.rank F E
⊢ #(Emb F E) = if ℵ₀ ≤ Module.rank F E then HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E) else Module.rank F E

Tactic:
split_ifs with h
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
h : ℵ₀ ≤ Module.rank F E
⊢ #(Emb F E) = HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)

Tactic:
cardinal_eq_two_pow_rank h

Premises used: Field.Emb.cardinal_eq_two_pow_rank
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
h : ℵ₀ ≤ Module.rank F E
⊢ #(Emb F E) = HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)

Tactic:
exact cardinal_eq_two_pow_rank h

Premises used: Field.Emb.cardinal_eq_two_pow_rank
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
h : ¬ℵ₀ ≤ Module.rank F E
⊢ IsNoetherian F E

Tactic:
rw [not_le, ← IsNoetherian.iff_rank_lt_aleph0] at h

Premises used: not_le, IsNoetherian.iff_rank_lt_aleph0
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
h : IsNoetherian F E
neg : #(Emb F E) = (↑(finrank F E) : Cardinal.{v})
neg₁ : (toNat : (a : Cardinal.{v}) → ℕ) #(Emb F E) = finrank F E
neg₂ : Nat.card.{v} (Emb F E) = finrank F E
neg₃ : finSepDegree F E = finrank F E
neg₄ neg₅ : finrank F E = finrank F E
⊢ #(Emb F E) = Module.rank F E

Tactic:
rw [← Module.finrank_eq_rank, ← toNat_eq_iff Module.finrank_pos.ne',
    ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable]

Premises used: Cardinal.toNat_eq_iff, Field.finSepDegree, Nat.card, Field.finSepDegree_eq_finrank_of_isSeparable, Module.finrank_eq_rank, LT.lt.ne', Module.finrank_pos
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
rank_inf : ℵ₀ ≤ sepDegree F E
rw :
  HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F ↥(separableClosure F E)) =
    HPow.hPow (α := Cardinal.{v}) 2 (sepDegree F E)
⊢ #(Emb F E) = HPow.hPow (α := Cardinal.{v}) 2 (sepDegree F E)

Tactic:
rw [← cardinal_separableClosure, cardinal_eq_two_pow_rank rank_inf]

Premises used: Field.Emb.cardinal_eq_two_pow_rank, Field.Emb.cardinal_separableClosure
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
rank_inf : ℵ₀ ≤ sepDegree F E
⊢ HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F ↥(separableClosure F E)) =
    HPow.hPow (α := Cardinal.{v}) 2 (sepDegree F E)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
rw :
  Eq.{v + 2} (α := Cardinal.{v})
    ((fun (c : Cardinal.{v}) ↦ if ℵ₀ ≤ c then HPow.hPow (α := Cardinal.{v}) 2 c else c)
      (Module.rank F ↥(separableClosure F E)))
    ((fun (c : Cardinal.{v}) ↦ if ℵ₀ ≤ c then HPow.hPow (α := Cardinal.{v}) 2 c else c) (sepDegree F E))
⊢ #(Emb F E) = (fun (c : Cardinal.{v}) ↦ if ℵ₀ ≤ c then HPow.hPow (α := Cardinal.{v}) 2 c else c) (sepDegree F E)

Tactic:
rw [← cardinal_separableClosure, cardinal_eq_of_isSeparable]

Premises used: Field.Emb.cardinal_eq_of_isSeparable, Field.Emb.cardinal_separableClosure
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
⊢ Eq.{v + 2} (α := Cardinal.{v})
    ((fun (c : Cardinal.{v}) ↦ if ℵ₀ ≤ c then HPow.hPow (α := Cardinal.{v}) 2 c else c)
      (Module.rank F ↥(separableClosure F E)))
    ((fun (c : Cardinal.{v}) ↦ if ℵ₀ ≤ c then HPow.hPow (α := Cardinal.{v}) 2 c else c) (sepDegree F E))

Tactic:
rfl
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Field α
⊢ IsPrimePow ‖α‖

Tactic:
FiniteField.isPrimePow_card α

Premises used: FiniteField.isPrimePow_card
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u_1
inst : Fintype α
⊢ Nonempty.{u_1 + 1} (Field α) ↔ IsPrimePow ‖α‖

Tactic:
⟨fun ⟨h⟩ => Fintype.isPrimePow_card_of_field, ?_⟩

Premises used: IsPrimePow, Fintype.card, Fintype.isPrimePow_card_of_field, _private.0.Fintype.nonempty_field_iff.match_1, Iff.intro
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u_1
inst : Fintype α
refine : IsPrimePow ‖α‖ → Nonempty.{u_1 + 1} (Field α)
⊢ Nonempty.{u_1 + 1} (Field α) ↔ IsPrimePow ‖α‖

Tactic:
refine ⟨fun ⟨h⟩ => Fintype.isPrimePow_card_of_field, ?_⟩
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
⊢ Fact (Nat.Prime p)

Tactic:
haveI := Fact.mk hp.nat_prime
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
this : Fact (Nat.Prime p)
haveI : ∀ (this : Fintype (GaloisField p n)), Nonempty.{u_1 + 1} (Field α)
⊢ Nonempty.{u_1 + 1} (Field α)

Tactic:
haveI : Fintype (GaloisField p n) := Fintype.ofFinite (GaloisField p n)
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
this_1 : Fact (Nat.Prime p)
this : Fintype (GaloisField p n)
⊢ Nonempty.{u_1 + 1} (Field α)

Tactic:
⟨(Fintype.equivOfCardEq
    (((Fintype.card_eq_nat_card).trans (GaloisField.card p n hn.ne')).trans hα)).symm.field⟩

Premises used: Equiv.field, Nonempty.intro, LT.lt.ne', GaloisField.card, Equiv.symm, Fintype.equivOfCardEq, Fintype.card_eq_nat_card, Eq.trans
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
this_1 : Fact (Nat.Prime p)
this : Fintype (GaloisField p n)
⊢ Nonempty.{u_1 + 1} (Field α)

Tactic:
exact ⟨(Fintype.equivOfCardEq
    (((Fintype.card_eq_nat_card).trans (GaloisField.card p n hn.ne')).trans hα)).symm.field⟩
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Ring α
⊢ ¬IsPrimePow ‖α‖ → ¬IsField α

Tactic:
mt fun h => Fintype.nonempty_field_iff.mp ⟨h.toField⟩

Premises used: mt, Nonempty.intro, Fintype.nonempty_field_iff, IsField.toField, Iff.mp
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u
inst : Infinite α
suffices : #α = #(FractionRing (MvPolynomial α (ULift.{u, 0} ℚ)))
⊢ Nonempty.{u + 1} (Field α)

Tactic:
suffices #α = #(FractionRing (MvPolynomial α <| ULift.{u} ℚ)) from
    (Cardinal.eq.1 this).map (·.field)
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u
inst : Infinite α
⊢ #α = #(FractionRing (MvPolynomial α (ULift.{u, 0} ℚ)))

Tactic:
simp
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u
rw : Nonempty.{u + 1} (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ (n : ℕ), #α = (↑n : Cardinal.{u}) ∧ IsPrimePow n
⊢ Nonempty.{u + 1} (Field α) ↔ IsPrimePow #α

Tactic:
rw [Cardinal.isPrimePow_iff]

Premises used: Cardinal.isPrimePow_iff
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u
inl : ∀ (h : Fintype α), Nonempty.{u + 1} (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ (n : ℕ), #α = (↑n : Cardinal.{u}) ∧ IsPrimePow n
inr : ∀ (h : Infinite α), Nonempty.{u + 1} (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ (n : ℕ), #α = (↑n : Cardinal.{u}) ∧ IsPrimePow n
⊢ Nonempty.{u + 1} (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ (n : ℕ), #α = (↑n : Cardinal.{u}) ∧ IsPrimePow n

Tactic:
obtain h | h := fintypeOrInfinite α

Premises used: fintypeOrInfinite
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u
h : Fintype α
⊢ Nonempty.{u + 1} (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ (n : ℕ), #α = (↑n : Cardinal.{u}) ∧ IsPrimePow n

Tactic:
simpa only [Cardinal.mk_fintype, Nat.cast_inj, exists_eq_left',
      Cardinal.natCast_lt_aleph0.not_ge, false_or] using Fintype.nonempty_field_iff

Premises used: exists_eq_left', false_or, Nat.cast_inj, Cardinal.natCast_lt_aleph0, Cardinal.mk_fintype, Fintype.nonempty_field_iff, LT.lt.not_ge
-- Module: Mathlib.FieldTheory.Cardinality
Goal:
α : Type u
h : Infinite α
⊢ Nonempty.{u + 1} (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ (n : ℕ), #α = (↑n : Cardinal.{u}) ∧ IsPrimePow n

Tactic:
simpa only [← Cardinal.infinite_iff, h, true_or, iff_true] using Infinite.nonempty_field

Premises used: true_or, iff_true, Cardinal.infinite_iff, Infinite.nonempty_field
-- 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 σ
haveI : ∀ (this : DecidableEq K), 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:
haveI : DecidableEq K := Classical.decEq K
-- 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 : DecidableEq K
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) f)
    (∑ x : σ → K, ∑ d ∈ f.support, coeff d f * ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ))

Tactic:
simp only [eval_eq']

Premises used: MvPolynomial.eval_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 : DecidableEq K
⊢ Eq.{u_1 + 1} (α := K)
    (∑ x : σ → K, ∑ d ∈ f.support, coeff d f * ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ))
    (∑ d ∈ f.support, ∑ x : σ → K, coeff d f * ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ))

Tactic:
sum_comm

Premises used: Finset.sum_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 : DecidableEq K
⊢ Eq.{u_1 + 1} (α := K)
    (∑ d ∈ f.support, ∑ x : σ → K, coeff d f * ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ)) 0

Tactic:
sum_eq_zero ?_

Premises used: Finset.sum_eq_zero
-- 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 : DecidableEq K
eval :
  ∀ x ∈ f.support,
    Eq.{u_1 + 1} (α := K) (∑ x_1 : σ → K, coeff x f * ∏ i : σ, HPow.hPow (β := ℕ) (x_1 i) ((x : (a : σ) → ℕ) i : ℕ)) 0
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (MvPolynomial.eval x : (a : MvPolynomial σ K) → K) f) 0

Tactic:
calc
    ∑ x, eval x f = ∑ x : σ → K, ∑ d ∈ f.support, f.coeff d * ∏ i, x i ^ d i := by
      simp only [eval_eq']
    _ = ∑ d ∈ f.support, ∑ x : σ → K, f.coeff d * ∏ i, x i ^ d i := sum_comm
    _ = 0 := sum_eq_zero ?_

Premises used: Finset.sum_eq_zero, MvPolynomial.support, Finset.sum_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 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ ∃ (i : σ), (d : (a : σ) → ℕ) i < q - 1

Tactic:
f.exists_degree_lt (q - 1) h hd

Premises used: HSub.hSub, Fintype.card, MvPolynomial.exists_degree_lt, OfNat.ofNat
-- 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 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
obtain :
  ∀ (i : σ) (hi : (d : (a : σ) → ℕ) i < q - 1),
    Eq.{u_1 + 1} (α := K) (∑ x : σ → K, coeff d f * ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ)) 0
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, coeff d f * ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ)) 0

Tactic:
obtain ⟨i, hi⟩ : ∃ i, d i < q - 1 := f.exists_degree_lt (q - 1) h hd
-- 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 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
⊢ ∑ x : σ → K, coeff d f * ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ) =
    coeff d f * ∑ x : σ → K, ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ)

Tactic:
(mul_sum ..).symm

Premises used: Finset.mul_sum, Eq.symm
-- 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 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
⊢ coeff d f * ∑ x : σ → K, ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ) = 0

Tactic:
(mul_eq_zero.mpr ∘ Or.inr) ?_

Premises used: Iff.mpr, Function.comp, mul_eq_zero, Or.inr
-- 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 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
x : Eq.{u_1 + 1} (α := K) (∑ x : σ → K, ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ)) 0
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, coeff d f * ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ)) 0

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

Premises used: Iff.mpr, Finset.mul_sum, HMul.hMul, Finset.univ, Function.comp, mul_eq_zero, MvPolynomial.coeff, Finset.prod, HPow.hPow, Eq.symm, DFunLike.coe, Finset.sum, Or.inr
-- 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 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ))
    (∑ x₀ : { j : σ // j ≠ i } → K,
      ∑ x : { x : σ → K // x ∘ Subtype.val = x₀ },
        ∏ j : σ, HPow.hPow (β := ℕ) ((↑x : σ → K) j) ((d : (a : σ) → ℕ) j : ℕ))

Tactic:
(Fintype.sum_fiberwise _ _).symm

Premises used: Fintype.sum_fiberwise, Eq.symm
-- 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 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
⊢ Eq.{u_1 + 1} (α := K)
    (∑ x₀ : { j : σ // j ≠ i } → K,
      ∑ x : { x : σ → K // x ∘ Subtype.val = x₀ },
        ∏ j : σ, HPow.hPow (β := ℕ) ((↑x : σ → K) j) ((d : (a : σ) → ℕ) j : ℕ))
    0

Tactic:
Fintype.sum_eq_zero _ ?_

Premises used: Fintype.sum_eq_zero
-- 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 : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
x :
  ∀ (a : { j : σ // j ≠ i } → K),
    Eq.{u_1 + 1} (α := K)
      (∑ x : { x : σ → K // x ∘ Subtype.val = a },
        ∏ j : σ, HPow.hPow (β := ℕ) ((↑x : σ → K) j) ((d : (a : σ) → ℕ) j : ℕ))
      0
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ)) 0

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

Premises used: Fintype.sum_eq_zero, Finset.univ, Finset.prod, HPow.hPow, Fintype.sum_fiberwise, Eq.symm, DFunLike.coe, Finset.sum
-- 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 : 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 : ℕ))
    (∑ a : K,
      ∏ j : σ,
        HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) j)
          ((d : (a : σ) → ℕ) j : ℕ))

Tactic:
(e.sum_comp _).symm

Premises used: Equiv.sum_comp, Eq.symm
-- 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 : 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)
    (∑ a : K,
      ∏ j : σ,
        HPow.hPow (α := K) (β := ℕ) ((↑((e : (a : K) → { x : σ → K // x ∘ Subtype.val = x₀ }) a) : σ → K) j)
          ((d : (a : σ) → ℕ) j : ℕ))
    (∑ a : K,
      (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)) *
        HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ))

Tactic:
Fintype.sum_congr _ _ ?_

Premises used: Fintype.sum_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 : 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 rw₁ :
  Eq.{u_1 + 1} (α := K)
    (∑ a : K,
      (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)) *
        HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ))
    (∑ i_1 : K,
      (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)) *
        HPow.hPow (β := ℕ) i_1 ((d : (a : σ) → ℕ) i : ℕ))
⊢ ∑ a : K,
      (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)) *
        HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ) =
    HMul.hMul (α := K) (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ))
      (∑ a : K, HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ))

Tactic:
rw [mul_sum]

Premises used: Finset.mul_sum
-- 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 : 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
rw₁ rw₂ : Eq.{u_1 + 1} (α := K) 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

Tactic:
rw [sum_pow_lt_card_sub_one K _ hi, mul_zero]

Premises used: FiniteField.sum_pow_lt_card_sub_one, MulZeroClass.mul_zero
-- 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 : 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
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 : ℕ)
⊢ Eq.{u_1 + 1} (α := K)
    (∑ x : { x : σ → K // x ∘ Subtype.val = x₀ },
      ∏ j : σ, HPow.hPow (β := ℕ) ((↑x : σ → K) j) ((d : (a : σ) → ℕ) j : ℕ))
    0

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]

Premises used: Finset.univ, Equiv.sum_comp, Fintype.sum_congr, Finset.prod, HPow.hPow, Eq.symm, Subtype.val, DFunLike.coe, Finset.sum