awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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}
⊢ 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})

Tactic:
refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_

Premises used: MvPolynomial.degrees_sub_le, MvPolynomial.degrees_prod_le, Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
s : σ
h : Membership.mem (γ := Finset σ) Finset.univ s
rw :
  (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}
⊢ 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}

Tactic:
rw [degrees_one, Multiset.zero_union]

Premises used: MvPolynomial.degrees_one, Multiset.zero_union
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
s : σ
h : 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}

Tactic:
le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)

Premises used: nsmul_le_nsmul_right, MvPolynomial.degrees_pow_le, le_trans
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
s : σ
h : Membership.mem (γ := Finset σ) Finset.univ s
refine :
  (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
        ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K)).degrees ≤
    {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}

Tactic:
refine le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)

Premises used: nsmul_le_nsmul_right, MvPolynomial.degrees_pow_le, le_trans
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
s : σ
h : 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:
degrees_sub_le.trans ?_

Premises used: MvPolynomial.degrees_sub_le, LE.le.trans
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
s : σ
h : Membership.mem (γ := Finset σ) Finset.univ s
refine : degrees.{u_1, u_2} (R := K) (X s) ∪ degrees.{u_1, u_2} (R := K) ((C : (a : K) → MvPolynomial σ K) (c s)) ≤ {s}
⊢ (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
        ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K)).degrees ≤
    {s}

Tactic:
refine degrees_sub_le.trans ?_

Premises used: MvPolynomial.degrees_sub_le, LE.le.trans
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
s : σ
h : Membership.mem (γ := Finset σ) Finset.univ s
rw : degrees.{u_1, u_2} (R := K) (X s) ≤ {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:
rw [degrees_C, Multiset.union_zero]

Premises used: MvPolynomial.degrees_C, Multiset.union_zero
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
s : σ
h : Membership.mem (γ := Finset σ) Finset.univ s
⊢ degrees.{u_1, u_2} (R := K) (X s) ≤ {s}

Tactic:
degrees_X' _

Premises used: MvPolynomial.degrees_X'
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
s : σ
h : Membership.mem (γ := Finset σ) Finset.univ s
⊢ degrees.{u_1, u_2} (R := K) (X s) ≤ {s}

Tactic:
exact degrees_X' _

Premises used: MvPolynomial.degrees_X'
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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}
refine₄ : ∀ (s : σ), Membership.mem (γ := Finset σ) Finset.univ s → degrees.{u_1, u_2} (R := K) (X 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})

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' _

Premises used: MvPolynomial.degrees_C, nsmul_le_nsmul_right, MvPolynomial.degrees_pow_le, MvPolynomial.degrees_sub_le, MvPolynomial.degrees_one, MvPolynomial.degrees_prod_le, Multiset.zero_union, Finset.sum_le_sum, MvPolynomial.degrees_X', LE.le.trans, Multiset.union_zero, le_trans
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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.{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)

Tactic:
rw [mem_restrictDegree_iff_sup, indicator]

Premises used: MvPolynomial.mem_restrictDegree_iff_sup, MvPolynomial.indicator
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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

Tactic:
le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)

Premises used: Multiset.count_le_of_le, MvPolynomial.degrees_indicator, le_of_eq, le_trans
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
refine : Multiset.count n (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}) = Fintype.card K - 1
⊢ 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

Tactic:
refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)

Premises used: Multiset.count_le_of_le, MvPolynomial.degrees_indicator, le_of_eq, le_trans
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
simp_rw : ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
⊢ Multiset.count n (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}) = Fintype.card K - 1

Tactic:
simp_rw [← Multiset.coe_countAddMonoidHom, map_sum,
    map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]

Premises used: Nat.cast_id, map_sum, nsmul_eq_mul, Multiset.coe_countAddMonoidHom, map_nsmul
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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
trans₂ : ℕ
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1

Tactic:
trans
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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}

Tactic:
Finset.sum_eq_single n ?_ ?_

Premises used: Finset.sum_eq_single
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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
refine_2 : n ∉ Finset.univ → (Fintype.card K - 1) * Multiset.count n {n} = 0
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = (Fintype.card K - 1) * Multiset.count n {n}

Tactic:
refine Finset.sum_eq_single n ?_ ?_

Premises used: Finset.sum_eq_single
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n b : σ
refine_1 : Membership.mem (γ := Finset σ) Finset.univ b → b ≠ n → (Fintype.card K - 1) * Multiset.count n {b} = 0
⊢ Membership.mem (γ := Finset σ) Finset.univ b → b ≠ n → (Fintype.card K - 1) * Multiset.count n {b} = 0

Tactic:
_
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n b : σ
h : Membership.mem (γ := Finset σ) Finset.univ b
ne : b ≠ n
⊢ (Fintype.card K - 1) * Multiset.count n {b} = 0

Tactic:
simp [ne, eqComm]

Premises used: eqComm
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
h : n ∉ Finset.univ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = 0

Tactic:
(h <| Finset.mem_univ _).elim

Premises used: Finset.mem_univ, False.elim
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
n : σ
h : n ∉ Finset.univ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = 0

Tactic:
exact (h <| Finset.mem_univ _).elim

Premises used: Finset.mem_univ, False.elim
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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
rw₁ rw₂ : Fintype.card K - 1 = Fintype.card K - 1
⊢ (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1

Tactic:
rw [Multiset.count_singleton_self, mul_one]

Premises used: Multiset.count_singleton_self, mul_one
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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
rw₉ : (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)

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]

Premises used: Nat.cast_id, Multiset.count_singleton_self, Multiset.count_le_of_le, MvPolynomial.degrees_indicator, map_sum, MvPolynomial.mem_restrictDegree_iff_sup, nsmul_eq_mul, Multiset.coe_countAddMonoidHom, mul_one, le_of_eq, map_nsmul, MvPolynomial.indicator, le_trans, eqComm
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : ∃ (x : σ), ¬a x = b x), ∃ (i : σ), a i ≠ b i
⊢ ∃ (i : σ), a i ≠ b i

Tactic:
rwa [Ne, funext_iff, not_forall] at h

Premises used: funext_iff, Ne, Classical.not_forall
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : Field K
a b : σ → K
h : a ≠ b
obtain :
  ∀ (i : σ) (hi : a i ≠ b i), Eq.{u_1 + 1} (α := K) ((eval a : (a : MvPolynomial σ K) → K) (indicator b) : K) (0 : K)
⊢ 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
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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
simp : ∃ (a_1 : σ), Membership.mem (γ := Finset σ) Finset.univ a_1 ∧ 1 - (a a_1 - b a_1) ^ (Fintype.card K - 1) = 0
⊢ Eq.{u_1 + 1} (α := K) ((eval a : (a : MvPolynomial σ K) → K) (indicator b) : K) (0 : K)

Tactic:
simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C,
    Finset.prod_eq_zero_iff]

Premises used: map_sub, map_pow, map_prod, Finset.prod_eq_zero_iff, map_one, MvPolynomial.eval_C, MvPolynomial.eval_X, MvPolynomial.indicator
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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

Tactic:
⟨i, Finset.mem_univ _, ?_⟩

Premises used: Finset.mem_univ, And.intro, Exists.intro
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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
refine : 1 - (a i - b i) ^ (Fintype.card K - 1) = 0
⊢ ∃ (a_1 : σ), Membership.mem (γ := Finset σ) Finset.univ a_1 ∧ 1 - (a a_1 - b a_1) ^ (Fintype.card K - 1) = 0

Tactic:
refine ⟨i, Finset.mem_univ _, ?_⟩
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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
⊢ 1 - (a i - b i) ^ (Fintype.card K - 1) = 0

Tactic:
rw [FiniteField.pow_card_sub_one_eq_one, sub_self]

Premises used: FiniteField.pow_card_sub_one_eq_one, sub_self
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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
ha₁ ha₂ ha₃ ha₄ : ¬a i = b i
⊢ a i - b i ≠ 0

Tactic:
rwa [Ne, sub_eq_zero]

Premises used: sub_eq_zero, Ne
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : CommSemiring K
p q : MvPolynomial σ K
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
⊢ (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

Tactic:
ext x
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : CommSemiring K
p q : MvPolynomial σ K
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:
simp
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : CommSemiring K
a : K
p : MvPolynomial σ K
h :
  ∀ (e : σ → K),
    (eval e : (a : MvPolynomial σ K) → K) (a • p) =
      HSMul.hSMul (α := K) (β := (σ → K) → K) ((RingHom.id K : (a : K) → K) a : K)
        (fun (e : σ → K) ↦ (eval e : (a : MvPolynomial σ K) → K) p) e
⊢ (fun (e : σ → K) ↦ (eval e : (a : MvPolynomial σ K) → K) (a • p)) =
    HSMul.hSMul (α := K) (β := (σ → K) → K) ((RingHom.id K : (a : K) → K) a : K) fun (e : σ → K) ↦
      (eval e : (a : MvPolynomial σ K) → K) p

Tactic:
ext e
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : CommSemiring K
a : K
p : MvPolynomial σ K
e : σ → K
⊢ (eval e : (a : MvPolynomial σ K) → K) (a • p) =
    HSMul.hSMul (α := K) (β := (σ → K) → K) ((RingHom.id K : (a : K) → K) a : K)
      (fun (e : σ → K) ↦ (eval e : (a : MvPolynomial σ K) → K) p) e

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
intro :
  ∀ (val : Fintype σ),
    Eq (α := Submodule K ((σ → K) → K)) (Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1))) ⊤
⊢ Eq (α := Submodule K ((σ → K) → K)) (Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1))) ⊤

Tactic:
cases nonempty_fintype σ

Premises used: nonempty_fintype
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
⊢ Eq (α := Submodule K ((σ → K) → K)) (Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1))) ⊤

Tactic:
top_unique (SetLike.le_def.2 fun e _ => mem_map.2 ?_)

Premises used: Iff.mpr, Submodule.mem_map, SetLike.le_def, top_unique
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
intro :
  ∀ (e : (σ → K) → K),
    Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ e →
      ∃ (y : MvPolynomial σ K),
        Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) y ∧
          (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K) y = e
⊢ Eq (α := Submodule K ((σ → K) → K)) (Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1))) ⊤

Tactic:
refine top_unique (SetLike.le_def.2 fun e _ => mem_map.2 ?_)

Premises used: Iff.mpr, Submodule.mem_map, SetLike.le_def, top_unique
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
e : (σ → K) → K
h : Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ e
⊢ ∃ (y : MvPolynomial σ K),
    Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) y ∧
      (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K) y = e

Tactic:
⟨∑ n : σ → K, e n • indicator n, ?_, ?_⟩

Premises used: Finset.univ, And.intro, Exists.intro, HSMul.hSMul, Finset.sum, MvPolynomial.indicator
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
e : (σ → K) → K
h : Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ e
intro :
  Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1))
    (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n))
intro₁ :
  (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K)
      (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n)) =
    e
⊢ ∃ (y : MvPolynomial σ K),
    Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) y ∧
      (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K) y = e

Tactic:
refine ⟨∑ n : σ → K, e n • indicator n, ?_, ?_⟩
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
e : (σ → K) → K
h : Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ e
⊢ Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1))
    (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n))

Tactic:
sum_mem fun c _ => smul_mem _ _ (indicator_mem_restrictDegree _)

Premises used: HSub.hSub, MvPolynomial.restrictDegree, Fintype.card, MvPolynomial.indicator_mem_restrictDegree, OfNat.ofNat, sum_mem, Submodule.smul_mem
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
e : (σ → K) → K
h : Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ e
⊢ Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1))
    (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n))

Tactic:
exact sum_mem fun c _ => smul_mem _ _ (indicator_mem_restrictDegree _)

Premises used: HSub.hSub, MvPolynomial.restrictDegree, Fintype.card, MvPolynomial.indicator_mem_restrictDegree, OfNat.ofNat, sum_mem, Submodule.smul_mem