awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  ∀ (h : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0),
    t.prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) t)
ht : a.leadingCoeff * prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t) ≠ 0
refine_2 : (Multiset.map leadingCoeff t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0

Tactic:
rwa [Polynomial.leadingCoeff_multiset_prod']

Premises used: Polynomial.leadingCoeff_multiset_prod'
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  ∀ (h : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0),
    t.prod.natDegree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.natDegree) t)
ht : a.leadingCoeff * prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t) ≠ 0
⊢ (Multiset.map leadingCoeff t).prod ≠ 0

Tactic:
apply right_ne_zero_of_mul ht

Premises used: right_ne_zero_of_mul
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
h : Ne.{u + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
⊢ Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) (Multiset.map f s.val))) 0

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
h : Ne.{u + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
⊢ natDegree.{u} (R := R) (∏ i ∈ s, f i) = ∑ i ∈ s, (f i).natDegree

Tactic:
simpa using natDegree_multiset_prod' (s.1.map f) (by simpa using h)

Premises used: Multiset.map, Finset.val, Polynomial.natDegree_multiset_prod'
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
h_1 : Nontrivial R
h₁ : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Tactic:
apply natDegree_multiset_prod'

Premises used: Polynomial.natDegree_multiset_prod'
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
h_1 : Nontrivial R
⊢ Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
inst_1 : Nontrivial R
h : ∀ f ∈ t, f.Monic
⊢ t.prod.Monic

Tactic:
simpa using monic_multiset_prod_of_monic _ _ h

Premises used: Polynomial.monic_multiset_prod_of_monic
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
inst_1 : Nontrivial R
h : ∀ f ∈ t, f.Monic
⊢ t.prod ≠ 0

Tactic:
have : t.prod ≠ 0 := Monic.ne_zero <| by simpa using monic_multiset_prod_of_monic _ _ h
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
inst_1 : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
rw : (↑t.prod.natDegree : WithBot ℕ) = (Multiset.map degree t).sum
rw₁ : (↑(Multiset.map natDegree t).sum : WithBot ℕ) = (Multiset.map degree t).sum
rw₂ : Multiset.sum (Multiset.map Nat.cast (Multiset.map natDegree t)) = (Multiset.map degree t).sum
rw₃ : Multiset.sum (Multiset.map (Nat.cast ∘ natDegree) t) = (Multiset.map degree t).sum
rw₄ : Multiset.sum (Multiset.map (fun (x : R[X]) ↦ (↑x.natDegree : WithBot ℕ)) t) = (Multiset.map degree t).sum
rw₅ rw₆ : (Multiset.map degree t).sum = (Multiset.map degree t).sum
⊢ t.prod.degree = (Multiset.map degree t).sum

Tactic:
rw [degree_eq_natDegree this, natDegree_multiset_prod_of_monic _ h, Nat.cast_multiset_sum,
    Multiset.map_map, Function.comp_def,
    Multiset.map_congr rfl (fun f hf => (degree_eq_natDegree (h f hf).ne_zero).symm)]

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_multiset_sum, Function.comp_def, Multiset.map_congr, Multiset.map_map, Eq.symm, Polynomial.natDegree_multiset_prod_of_monic, rfl, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
h : ∀ i ∈ s, (f i).Monic
⊢ ∀ f_1 ∈ Multiset.map f s.val, f_1.Monic

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
h : ∀ i ∈ s, (f i).Monic
⊢ natDegree.{u} (R := R) (∏ i ∈ s, f i) = ∑ i ∈ s, (f i).natDegree

Tactic:
simpa using natDegree_multiset_prod_of_monic (s.1.map f) (by simpa using h)

Premises used: Multiset.map, Finset.val, Polynomial.natDegree_multiset_prod_of_monic
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
inst_1 : Nontrivial R
h : ∀ i ∈ s, (f i).Monic
⊢ ∀ f_1 ∈ Multiset.map f s.val, f_1.Monic

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
inst_1 : Nontrivial R
h : ∀ i ∈ s, (f i).Monic
⊢ degree.{u} (R := R) (∏ i ∈ s, f i) = ∑ i ∈ s, (f i).degree

Tactic:
simpa using degree_multiset_prod_of_monic (s.1.map f) (by simpa using h)

Premises used: Multiset.map, Polynomial.degree_multiset_prod_of_monic, Finset.val
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
n : ℕ
hl : ∀ p ∈ t, p.natDegree ≤ n
h :
  ∀ (a : List R[X]) (hl : ∀ (p : R[X]), Membership.mem (γ := Multiset R[X]) ⟦a⟧ p → p.natDegree ≤ n),
    (prod ⟦a⟧).coeff (Multiset.card ⟦a⟧ * n) = prod (Multiset.map (fun (p : R[X]) ↦ p.coeff n) ⟦a⟧)
⊢ t.prod.coeff (t.card * n) = prod (Multiset.map (fun (p : R[X]) ↦ p.coeff n) t)

Tactic:
induction t using Quotient.inductionOn
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
n : ℕ
a : List R[X]
hl : ∀ (p : R[X]), Membership.mem (γ := Multiset R[X]) ⟦a⟧ p → p.natDegree ≤ n
⊢ (prod ⟦a⟧).coeff (Multiset.card ⟦a⟧ * n) = prod (Multiset.map (fun (p : R[X]) ↦ p.coeff n) ⟦a⟧)

Tactic:
simpa using coeff_list_prod_of_natDegree_le _ _ hl

Premises used: Polynomial.coeff_list_prod_of_natDegree_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
n : ℕ
h : ∀ p ∈ s, (f p).natDegree ≤ n
obtain :
  ∀ (l : Multiset ι) (hl : l.Nodup) (h : ∀ p ∈ { val := l, nodup := hl : Finset ι }, (f p).natDegree ≤ n),
    Eq.{u + 1} (α := R)
      (coeff (∏ i ∈ { val := l, nodup := hl : Finset ι }, f i) (#{ val := l, nodup := hl : Finset ι } * n))
      (∏ i ∈ { val := l, nodup := hl : Finset ι }, (f i).coeff n)
⊢ Eq.{u + 1} (α := R) (coeff (∏ i ∈ s, f i) (#s * n)) (∏ i ∈ s, (f i).coeff n)

Tactic:
obtain ⟨l, hl⟩ := s
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
inst : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl : Finset ι }, (f p).natDegree ≤ n
⊢ (Multiset.map f l).prod.coeff ((Multiset.map f l).card * n) =
    prod (Multiset.map (fun (p : R[X]) ↦ p.coeff n) (Multiset.map f l))

Tactic:
coeff_multiset_prod_of_natDegree_le (l.map f) n ?_

Premises used: Multiset.map, Polynomial.coeff_multiset_prod_of_natDegree_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
inst : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl : Finset ι }, (f p).natDegree ≤ n
h₁ : #{ val := l, nodup := hl : Finset ι } = (Multiset.map f l).card
h₂ :
  Eq (α := R) (∏ i ∈ { val := l, nodup := hl : Finset ι }, (f i).coeff n)
    (prod (Multiset.map (fun (p : R[X]) ↦ p.coeff n) (Multiset.map f l)))
convert! : ∀ p ∈ Multiset.map f l, p.natDegree ≤ n
⊢ Eq.{u + 1} (α := R)
    (coeff (∏ i ∈ { val := l, nodup := hl : Finset ι }, f i) (#{ val := l, nodup := hl : Finset ι } * n))
    (∏ i ∈ { val := l, nodup := hl : Finset ι }, (f i).coeff n)

Tactic:
convert! coeff_multiset_prod_of_natDegree_le (l.map f) n ?_

Premises used: Multiset.map, Polynomial.coeff_multiset_prod_of_natDegree_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
inst : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl : Finset ι }, (f p).natDegree ≤ n
⊢ #{ val := l, nodup := hl : Finset ι } = (Multiset.map f l).card

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
inst : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl : Finset ι }, (f p).natDegree ≤ n
⊢ Eq (α := R) (∏ i ∈ { val := l, nodup := hl : Finset ι }, (f i).coeff n)
    (prod (Multiset.map (fun (p : R[X]) ↦ p.coeff n) (Multiset.map f l)))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
inst : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl : Finset ι }, (f p).natDegree ≤ n
⊢ ∀ p ∈ Multiset.map f l, p.natDegree ≤ n

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
⊢ t.prod.coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t)

Tactic:
Multiset.induction_on t ?_ fun a t ht => ?_

Premises used: Multiset.induction_on
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
refine_1 : Eq.{u + 1} (α := R) (coeff (prod 0) 0) (prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) 0))
refine_2 :
  ∀ (a : R[X]) (t : Multiset R[X]) (ht : t.prod.coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t)),
    (a ::ₘ t).prod.coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) (a ::ₘ t))
⊢ t.prod.coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t)

Tactic:
refine Multiset.induction_on t ?_ fun a t ht => ?_
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
⊢ Eq.{u + 1} (α := R) (coeff (prod 0) 0) (prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
t_1 : Multiset R[X]
a : R[X]
t : Multiset R[X]
ht : t.prod.coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t)
refine_2 : (a * t.prod).coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) (a ::ₘ t))
refine_2₁ : (a * t.prod).coeff 0 = (a.coeff 0 ::ₘ Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t).prod
refine_2₂ : (a * t.prod).coeff 0 = a.coeff 0 * prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t)
refine_2₃ : a.coeff 0 * t.prod.coeff 0 = a.coeff 0 * prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t)
refine_2₄ refine_2₅ :
  a.coeff 0 * prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t) =
    a.coeff 0 * prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t)
⊢ (a ::ₘ t).prod.coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) (a ::ₘ t))

Tactic:
rw [Multiset.prod_cons, Multiset.map_cons, Multiset.prod_cons, Polynomial.mul_coeff_zero, ht]

Premises used: Multiset.map_cons, Multiset.prod_cons, Polynomial.mul_coeff_zero
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
⊢ Eq.{u + 1} (α := R) (coeff (∏ i ∈ s, f i) 0) (∏ i ∈ s, (f i).coeff 0)

Tactic:
simpa using coeff_zero_multiset_prod (s.1.map f)

Premises used: Multiset.map, Finset.val, Polynomial.coeff_zero_multiset_prod
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
rw :
  Multiset.sum
      (Multiset.map (fun (i : R) ↦ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).nextCoeff) t) =
    -t.sum
h : ∀ i ∈ t, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).Monic
⊢ nextCoeff
      (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t)) =
    -t.sum

Tactic:
rw [nextCoeff_multiset_prod]

Premises used: Polynomial.Monic.nextCoeff_multiset_prod
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
simp : Multiset.sum (Multiset.map (fun (x : R) ↦ -x) t) = -t.sum
⊢ Multiset.sum
      (Multiset.map (fun (i : R) ↦ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).nextCoeff) t) =
    -t.sum

Tactic:
simp only [nextCoeff_X_sub_C]

Premises used: Polynomial.nextCoeff_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
⊢ Multiset.sum (Multiset.map (fun (x : R) ↦ -x) t) = -t.sum

Tactic:
t.sum_hom (-AddMonoidHom.id R)

Premises used: Multiset.sum, Multiset.foldr, AddMonoidHom.id, Multiset.sum_hom, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
⊢ Multiset.sum (Multiset.map (fun (x : R) ↦ -x) t) = -t.sum

Tactic:
exact t.sum_hom (-AddMonoidHom.id R)

Premises used: AddMonoidHom.id, Multiset.sum_hom, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
i : R
h : i ∈ t
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).Monic

Tactic:
apply monic_X_sub_C

Premises used: Polynomial.monic_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
inst : CommRing R
s : Finset ι
f : ι → R
⊢ Eq.{u + 1} (α := R) (nextCoeff (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f i) : R[X])))
    (-∑ i ∈ s, f i)

Tactic:
simpa using multiset_prod_X_sub_C_nextCoeff (s.1.map f)

Premises used: Multiset.map, Finset.val, Polynomial.multiset_prod_X_sub_C_nextCoeff
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial R
⊢ Multiset R

Tactic:
assumption
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h_1 : Nontrivial R
h :
  Eq (α := R)
    (coeff (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t))
      (t.card - 1))
    (nextCoeff
      (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t)))
⊢ coeff (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t))
      (t.card - 1) =
    -t.sum

Tactic:
convert! multiset_prod_X_sub_C_nextCoeff (by assumption)

Premises used: Polynomial.multiset_prod_X_sub_C_nextCoeff
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h_1 : Nontrivial R
h :
  Eq (α := R)
    (coeff (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t))
      (t.card - 1))
    (coeff (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t))
      (natDegree (R := R)
          (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t)) -
        1))
h₁ :
  ¬natDegree (R := R)
        (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t)) =
      0
⊢ Eq (α := R)
    (coeff (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t))
      (t.card - 1))
    (nextCoeff
      (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t)))

Tactic:
rw [nextCoeff, if_neg]

Premises used: Polynomial.nextCoeff, if_neg
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h_1 : Nontrivial R
h :
  ¬(Multiset.map (α := R[X]) natDegree
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t)).sum =
      0
h₁ :
  ∀ (f : R[X]),
    Membership.mem (γ := Multiset R[X])
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t) f →
      f.Monic
⊢ ¬natDegree (R := R)
        (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t)) =
      0

Tactic:
rw [natDegree_multiset_prod_of_monic]

Premises used: Polynomial.natDegree_multiset_prod_of_monic
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h_1 : Nontrivial R
h : ∀ (f : R[X]), (∃ a ∈ t, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = f) → f.Monic
⊢ ∀ (f : R[X]),
    Membership.mem (γ := Multiset R[X])
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t) f →
      f.Monic

Tactic:
simp only [Multiset.mem_map]

Premises used: Multiset.mem_map
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial R
w : R
left : w ∈ t
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) w : R[X])).Monic

Tactic:
apply monic_X_sub_C

Premises used: Polynomial.monic_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h_1 : Nontrivial R
h :
  ¬∀ (x : ℕ),
      (∃ (a : R[X]),
          (∃ a_1 ∈ t, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a_1 : R[X]) = a) ∧ a.natDegree = x) →
        x = 0
⊢ ¬(Multiset.map (α := R[X]) natDegree
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t)).sum =
      0

Tactic:
simp_rw [Multiset.sum_eq_zero_iff, Multiset.mem_map]

Premises used: Multiset.mem_map, Multiset.sum_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h_1 : Nontrivial R
h :
  ∀ (x : R) (hx : x ∈ t),
    ¬∀ (x : ℕ),
        (∃ (a : R[X]),
            (∃ a_1 ∈ t, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a_1 : R[X]) = a) ∧ a.natDegree = x) →
          x = 0
⊢ ¬∀ (x : ℕ),
      (∃ (a : R[X]),
          (∃ a_1 ∈ t, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a_1 : R[X]) = a) ∧ a.natDegree = x) →
        x = 0

Tactic:
obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp ht

Premises used: Iff.mp, Multiset.card_pos_iff_exists_mem
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial R
x : R
hx : x ∈ t
⊢ ¬∀ (x : ℕ),
      (∃ (a : R[X]),
          (∃ a_1 ∈ t, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a_1 : R[X]) = a) ∧ a.natDegree = x) →
        x = 0

Tactic:
fun h => one_ne_zero <| h 1 ⟨_, ⟨x, hx, rfl⟩, natDegree_X_sub_C _⟩

Premises used: Polynomial.C, HSub.hSub, Polynomial.natDegree_X_sub_C, And.intro, Exists.intro, one_ne_zero, OfNat.ofNat, Polynomial.X, DFunLike.coe, Not, rfl
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial R
x : R
hx : x ∈ t
⊢ ¬∀ (x : ℕ),
      (∃ (a : R[X]),
          (∃ a_1 ∈ t, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a_1 : R[X]) = a) ∧ a.natDegree = x) →
        x = 0

Tactic:
exact fun h => one_ne_zero <| h 1 ⟨_, ⟨x, hx, rfl⟩, natDegree_X_sub_C _⟩

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h_1 : Nontrivial R
h :
  t.card =
    natDegree (R := R)
      (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t))
⊢ Eq (α := R)
    (coeff (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t))
      (t.card - 1))
    (coeff (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t))
      (natDegree (R := R)
          (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t)) -
        1))

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h_1 : Nontrivial R
h :
  t.card =
    (Multiset.map (α := R[X]) natDegree
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t)).sum
h₁ :
  ∀ (f : R[X]),
    Membership.mem (γ := Multiset R[X])
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t) f →
      f.Monic
⊢ t.card =
    natDegree (R := R)
      (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t))

Tactic:
rw [natDegree_multiset_prod_of_monic]

Premises used: Polynomial.natDegree_multiset_prod_of_monic
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial R
⊢ t.card =
    (Multiset.map (α := R[X]) natDegree
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t)).sum

Tactic:
simp [monic_X_sub_C]

Premises used: Polynomial.monic_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial R
⊢ ∀ (f : R[X]),
    Membership.mem (γ := Multiset R[X])
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) t) f →
      f.Monic

Tactic:
simp [monic_X_sub_C]

Premises used: Polynomial.monic_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
inst : CommRing R
s : Finset ι
f : ι → R
hs : 0 < #s
⊢ 0 < (Multiset.map f s.val).card

Tactic:
simpa using hs
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
inst : CommRing R
s : Finset ι
f : ι → R
hs : 0 < #s
⊢ Eq.{u + 1} (α := R)
    (coeff (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f i) : R[X])) (#s - 1)) (-∑ i ∈ s, f i)

Tactic:
simpa using multiset_prod_X_sub_C_coeff_card_pred (s.1.map f) (by simpa using hs)

Premises used: Multiset.map, Finset.val, Polynomial.multiset_prod_X_sub_C_coeff_card_pred
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
a :
  degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) ≤
    s.sup fun (i : ι) ↦ (f i).degree
a₁ :
  (s.sup fun (i : ι) ↦ (f i).degree) ≤
    degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
⊢ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) =
    s.sup fun (i : ι) ↦ (f i).degree

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
⊢ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) ≤
    s.sup fun (i : ι) ↦ (f i).degree

Tactic:
(degree_sum_le s _).trans <| Finset.sup_le fun i hi ↦ (degree_smul_le _ _).trans <|
      degree_map_le.trans <| Finset.le_sup (f := fun i ↦ (f i).degree) hi

Premises used: Polynomial.degree_map_le, Algebra.algebraMap, Polynomial.degree_sum_le, Finset.sup_le, Polynomial.degree_smul_le, Polynomial.map, LE.le.trans, Finset.le_sup