awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
refine :
  ∀ (s : σ),
    Membership.mem (γ := Finset σ) Finset.univ s →
      degrees.{u_1, u_2} (R := K) 1 ∪
          (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
                ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
              (Fintype.card K - 1)).degrees ≤
        HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
refine₁ :
  ∀ (s : σ),
    Membership.mem (γ := Finset σ) Finset.univ s →
      (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
              ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
            (Fintype.card K - 1)).degrees ≤
        HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
⊢ LE.le.{u_2} (α := Multiset σ)
    (degrees.{u_1, u_2} (R := K)
      (∏ n : σ,
        (1 -
          HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
              ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
            (Fintype.card K - 1))))
    (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s})
have refine₂ : ∀ (s : σ),
  Membership.mem (γ := Finset σ) Finset.univ s →
    (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
          ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K)).degrees ≤
      {s}
Tactic: classical
  refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_
  rw [degrees_one, Multiset.zero_union]
  refine le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)
  refine degrees_sub_le.trans ?_
  rw [degrees_C, Multiset.union_zero]
  exact degrees_X' _
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
refine :
  ∀ (s : σ),
    Membership.mem (γ := Finset σ) Finset.univ s →
      degrees.{u_1, u_2} (R := K) 1 ∪
          (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
                ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
              (Fintype.card K - 1)).degrees ≤
        HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
refine₁ :
  ∀ (s : σ),
    Membership.mem (γ := Finset σ) Finset.univ s →
      (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
              ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
            (Fintype.card K - 1)).degrees ≤
        HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
refine₂ :
  ∀ (s : σ),
    Membership.mem (γ := Finset σ) Finset.univ s →
      (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
            ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K)).degrees ≤
        {s}
⊢ LE.le.{u_2} (α := Multiset σ)
    (degrees.{u_1, u_2} (R := K)
      (∏ n : σ,
        (1 -
          HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
              ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
            (Fintype.card K - 1))))
    (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s})
have refine₃ : ∀ (s : σ),
  Membership.mem (γ := Finset σ) Finset.univ s →
    degrees.{u_1, u_2} (R := K) (X s) ∪ degrees.{u_1, u_2} (R := K) ((C : (a : K) → MvPolynomial σ K) (c s)) ≤ {s}
Tactic: classical
  refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_
  rw [degrees_one, Multiset.zero_union]
  refine le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)
  refine degrees_sub_le.trans ?_
  rw [degrees_C, Multiset.union_zero]
  exact degrees_X' _
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
refine :
  ∀ (s : σ),
    Membership.mem (γ := Finset σ) Finset.univ s →
      degrees.{u_1, u_2} (R := K) 1 ∪
          (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
                ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
              (Fintype.card K - 1)).degrees ≤
        HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
refine₁ :
  ∀ (s : σ),
    Membership.mem (γ := Finset σ) Finset.univ s →
      (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
              ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
            (Fintype.card K - 1)).degrees ≤
        HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
refine₂ :
  ∀ (s : σ),
    Membership.mem (γ := Finset σ) Finset.univ s →
      (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
            ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K)).degrees ≤
        {s}
refine₃ :
  ∀ (s : σ),
    Membership.mem (γ := Finset σ) Finset.univ s →
      degrees.{u_1, u_2} (R := K) (X s) ∪ degrees.{u_1, u_2} (R := K) ((C : (a : K) → MvPolynomial σ K) (c s)) ≤ {s}
⊢ LE.le.{u_2} (α := Multiset σ)
    (degrees.{u_1, u_2} (R := K)
      (∏ n : σ,
        (1 -
          HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
              ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
            (Fintype.card K - 1))))
    (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s})
have refine₄ : ∀ (s : σ), Membership.mem (γ := Finset σ) Finset.univ s → degrees.{u_1, u_2} (R := K) (X s) ≤ {s}
Tactic: classical
  refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_
  rw [degrees_one, Multiset.zero_union]
  refine le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)
  refine degrees_sub_le.trans ?_
  rw [degrees_C, Multiset.union_zero]
  exact degrees_X' _
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
⊢ Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) (indicator c)
have rw : ∀ (i : σ),
  Multiset.count i
      (degrees.{u_1, u_2} (R := K)
        (∏ n : σ,
          (1 -
            HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
                ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
              (Fintype.card K - 1)))) ≤
    Fintype.card K - 1
Tactic: rw [mem_restrictDegree_iff_sup, indicator]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
⊢ Multiset.count n
      (degrees.{u_1, u_2} (R := K)
        (∏ n : σ,
          (1 -
            HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
                ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
              (Fintype.card K - 1)))) ≤
    Fintype.card K - 1
have refine : Multiset.count n (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}) = Fintype.card K - 1
Tactic: refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
⊢ Multiset.count n (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}) = Fintype.card K - 1
have simp_rw : ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
Tactic: simp_rw [← Multiset.coe_countAddMonoidHom, map_sum,
    map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
have trans : ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = (Fintype.card K - 1) * Multiset.count n {n}
Tactic: trans
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
trans : ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = (Fintype.card K - 1) * Multiset.count n {n}
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
have trans₁ : (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1
Tactic: trans
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
trans : ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = (Fintype.card K - 1) * Multiset.count n {n}
trans₁ : (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
have trans₂ : ℕ
Tactic: trans
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = (Fintype.card K - 1) * Multiset.count n {n}
have refine_1 : ∀ (b : σ), Membership.mem (γ := Finset σ) Finset.univ b → b ≠ n → (Fintype.card K - 1) * Multiset.count n {b} = 0
Tactic: refine Finset.sum_eq_single n ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
refine_1 :
  ∀ (b : σ), Membership.mem (γ := Finset σ) Finset.univ b → b ≠ n → (Fintype.card K - 1) * Multiset.count n {b} = 0
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = (Fintype.card K - 1) * Multiset.count n {n}
have refine_2 : n ∉ Finset.univ → (Fintype.card K - 1) * Multiset.count n {n} = 0
Tactic: refine Finset.sum_eq_single n ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1
have rw : (Fintype.card K - 1) * 1 = Fintype.card K - 1
Tactic: rw [Multiset.count_singleton_self, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
rw : (Fintype.card K - 1) * 1 = Fintype.card K - 1
⊢ (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1
have rw₁ : Fintype.card K - 1 = Fintype.card K - 1
Tactic: rw [Multiset.count_singleton_self, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
⊢ Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) (indicator c)
have rw : ∀ (i : σ), Multiset.count i (degrees (indicator c)) ≤ Fintype.card K - 1
Tactic: classical
  rw [mem_restrictDegree_iff_sup, indicator]
  intro n
  refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)
  simp_rw [← Multiset.coe_countAddMonoidHom, map_sum,
    map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
  trans
  · refine Finset.sum_eq_single n ?_ ?_
    · intro b _ ne
      simp [ne, eqComm]
    · intro h; exact (h <| Finset.mem_univ _).elim
  · rw [Multiset.count_singleton_self, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
rw : ∀ (i : σ), Multiset.count i (degrees (indicator c)) ≤ Fintype.card K - 1
⊢ Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) (indicator c)
have rw₁ : ∀ (i : σ),
  Multiset.count i
      (degrees.{u_1, u_2} (R := K)
        (∏ n : σ,
          (1 -
            HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
                ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
              (Fintype.card K - 1)))) ≤
    Fintype.card K - 1
Tactic: classical
  rw [mem_restrictDegree_iff_sup, indicator]
  intro n
  refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)
  simp_rw [← Multiset.coe_countAddMonoidHom, map_sum,
    map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
  trans
  · refine Finset.sum_eq_single n ?_ ?_
    · intro b _ ne
      simp [ne, eqComm]
    · intro h; exact (h <| Finset.mem_univ _).elim
  · rw [Multiset.count_singleton_self, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
rw : ∀ (i : σ), Multiset.count i (degrees (indicator c)) ≤ Fintype.card K - 1
rw₁ rw₂ rw₃ rw₄ :
  ∀ (n : σ),
    Multiset.count n
        (degrees.{u_1, u_2} (R := K)
          (∏ n : σ,
            (1 -
              HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
                  ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
                (Fintype.card K - 1)))) ≤
      Fintype.card K - 1
⊢ Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) (indicator c)
have rw₅ : ∀ (n : σ), Multiset.count n (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}) = Fintype.card K - 1
Tactic: classical
  rw [mem_restrictDegree_iff_sup, indicator]
  intro n
  refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)
  simp_rw [← Multiset.coe_countAddMonoidHom, map_sum,
    map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
  trans
  · refine Finset.sum_eq_single n ?_ ?_
    · intro b _ ne
      simp [ne, eqComm]
    · intro h; exact (h <| Finset.mem_univ _).elim
  · rw [Multiset.count_singleton_self, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
rw : ∀ (i : σ), Multiset.count i (degrees (indicator c)) ≤ Fintype.card K - 1
rw₁ rw₂ rw₃ rw₄ :
  ∀ (n : σ),
    Multiset.count n
        (degrees.{u_1, u_2} (R := K)
          (∏ n : σ,
            (1 -
              HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
                  ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
                (Fintype.card K - 1)))) ≤
      Fintype.card K - 1
rw₅ : ∀ (n : σ), Multiset.count n (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}) = Fintype.card K - 1
⊢ Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) (indicator c)
have rw₆ : ∀ (n : σ), ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
Tactic: classical
  rw [mem_restrictDegree_iff_sup, indicator]
  intro n
  refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)
  simp_rw [← Multiset.coe_countAddMonoidHom, map_sum,
    map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
  trans
  · refine Finset.sum_eq_single n ?_ ?_
    · intro b _ ne
      simp [ne, eqComm]
    · intro h; exact (h <| Finset.mem_univ _).elim
  · rw [Multiset.count_singleton_self, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
rw : ∀ (i : σ), Multiset.count i (degrees (indicator c)) ≤ Fintype.card K - 1
rw₁ rw₂ rw₃ rw₄ :
  ∀ (n : σ),
    Multiset.count n
        (degrees.{u_1, u_2} (R := K)
          (∏ n : σ,
            (1 -
              HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
                  ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
                (Fintype.card K - 1)))) ≤
      Fintype.card K - 1
rw₅ : ∀ (n : σ), Multiset.count n (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}) = Fintype.card K - 1
rw₆ : ∀ (n : σ), ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
⊢ Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) (indicator c)
have rw₇ : ∀ (n : σ), ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = (Fintype.card K - 1) * Multiset.count n {n}
Tactic: classical
  rw [mem_restrictDegree_iff_sup, indicator]
  intro n
  refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)
  simp_rw [← Multiset.coe_countAddMonoidHom, map_sum,
    map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
  trans
  · refine Finset.sum_eq_single n ?_ ?_
    · intro b _ ne
      simp [ne, eqComm]
    · intro h; exact (h <| Finset.mem_univ _).elim
  · rw [Multiset.count_singleton_self, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
rw : ∀ (i : σ), Multiset.count i (degrees (indicator c)) ≤ Fintype.card K - 1
rw₁ rw₂ rw₃ rw₄ :
  ∀ (n : σ),
    Multiset.count n
        (degrees.{u_1, u_2} (R := K)
          (∏ n : σ,
            (1 -
              HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
                  ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
                (Fintype.card K - 1)))) ≤
      Fintype.card K - 1
rw₅ : ∀ (n : σ), Multiset.count n (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}) = Fintype.card K - 1
rw₆ : ∀ (n : σ), ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
rw₇ : ∀ (n : σ), ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = (Fintype.card K - 1) * Multiset.count n {n}
⊢ Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) (indicator c)
have rw₈ : ∀ (n : σ), (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1
Tactic: classical
  rw [mem_restrictDegree_iff_sup, indicator]
  intro n
  refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)
  simp_rw [← Multiset.coe_countAddMonoidHom, map_sum,
    map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
  trans
  · refine Finset.sum_eq_single n ?_ ?_
    · intro b _ ne
      simp [ne, eqComm]
    · intro h; exact (h <| Finset.mem_univ _).elim
  · rw [Multiset.count_singleton_self, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
rw : ∀ (i : σ), Multiset.count i (degrees (indicator c)) ≤ Fintype.card K - 1
rw₁ rw₂ rw₃ rw₄ :
  ∀ (n : σ),
    Multiset.count n
        (degrees.{u_1, u_2} (R := K)
          (∏ n : σ,
            (1 -
              HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
                  ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
                (Fintype.card K - 1)))) ≤
      Fintype.card K - 1
rw₅ : ∀ (n : σ), Multiset.count n (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}) = Fintype.card K - 1
rw₆ : ∀ (n : σ), ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
rw₇ : ∀ (n : σ), ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = (Fintype.card K - 1) * Multiset.count n {n}
rw₈ : ∀ (n : σ), (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1
⊢ Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) (indicator c)
have rw₉ : (n : σ) → ℕ
Tactic: classical
  rw [mem_restrictDegree_iff_sup, indicator]
  intro n
  refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)
  simp_rw [← Multiset.coe_countAddMonoidHom, map_sum,
    map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
  trans
  · refine Finset.sum_eq_single n ?_ ?_
    · intro b _ ne
      simp [ne, eqComm]
    · intro h; exact (h <| Finset.mem_univ _).elim
  · rw [Multiset.count_singleton_self, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : Field K
a b : σ → K
h : a ≠ b
⊢ ∃ (i : σ), a i ≠ b i
have rwa : ∀ (h : ¬a = b), ∃ (i : σ), a i ≠ b i
Tactic: rwa [Ne, funext_iff, not_forall] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : Field K
a b : σ → K
h : a ≠ b
rwa : ∀ (h : ¬a = b), ∃ (i : σ), a i ≠ b i
⊢ ∃ (i : σ), a i ≠ b i
have rwa₁ : ∀ (h : ¬∀ (x : σ), a x = b x), ∃ (i : σ), a i ≠ b i
Tactic: rwa [Ne, funext_iff, not_forall] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : Field K
a b : σ → K
h : a ≠ b
rwa : ∀ (h : ¬a = b), ∃ (i : σ), a i ≠ b i
rwa₁ : ∀ (h : ¬∀ (x : σ), a x = b x), ∃ (i : σ), a i ≠ b i
⊢ ∃ (i : σ), a i ≠ b i
have rwa₂ : ∀ (h : ∃ (x : σ), ¬a x = b x), ∃ (i : σ), a i ≠ b i
Tactic: rwa [Ne, funext_iff, not_forall] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : Field K
a b : σ → K
h : a ≠ b
⊢ Eq.{u_1 + 1} (α := K) ((eval a : (a : MvPolynomial σ K) → K) (indicator b) : K) (0 : K)
have obtain : ∀ (i : σ) (hi : a i ≠ b i), Eq.{u_1 + 1} (α := K) ((eval a : (a : MvPolynomial σ K) → K) (indicator b) : K) (0 : K)
Tactic: obtain ⟨i, hi⟩ : ∃ i, a i ≠ b i := by rwa [Ne, funext_iff, not_forall] at h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ Eq.{u_1 + 1} (α := K) ((eval a : (a : MvPolynomial σ K) → K) (indicator b) : K) (0 : K)
have simp : ∃ (a_1 : σ), Membership.mem (γ := Finset σ) Finset.univ a_1 ∧ 1 - (a a_1 - b a_1) ^ (Fintype.card K - 1) = 0
Tactic: simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C,
    Finset.prod_eq_zero_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ ∃ (a_1 : σ), Membership.mem (γ := Finset σ) Finset.univ a_1 ∧ 1 - (a a_1 - b a_1) ^ (Fintype.card K - 1) = 0
have refine : 1 - (a i - b i) ^ (Fintype.card K - 1) = 0
Tactic: refine ⟨i, Finset.mem_univ _, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ 1 - (a i - b i) ^ (Fintype.card K - 1) = 0
have ha : a i - b i ≠ 0
Tactic: rw [FiniteField.pow_card_sub_one_eq_one, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ a i - b i ≠ 0
have ha : ¬a i - b i = 0
Tactic: rwa [Ne, sub_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
ha : ¬a i - b i = 0
⊢ a i - b i ≠ 0
have ha₁ : ¬a i = b i
Tactic: rwa [Ne, sub_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : CommSemiring K
p q : MvPolynomial σ K
⊢ (fun (e : σ → K) ↦ (eval e : (a : MvPolynomial σ K) → K) (p + q)) =
    HAdd.hAdd (α := (σ → K) → K) (fun (e : σ → K) ↦ (eval e : (a : MvPolynomial σ K) → K) p) fun (e : σ → K) ↦
      (eval e : (a : MvPolynomial σ K) → K) q
have h : ∀ (x : σ → K),
  (eval x : (a : MvPolynomial σ K) → K) (p + q) =
    HAdd.hAdd (α := (σ → K) → K) (β := (σ → K) → K) (fun (e : σ → K) ↦ (eval e : (a : MvPolynomial σ K) → K) p)
      (fun (e : σ → K) ↦ (eval e : (a : MvPolynomial σ K) → K) q) x
Tactic: ext x