awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ t.prod.degree = (Multiset.map degree t).sum
have rw₃ : Multiset.sum (Multiset.map (Nat.cast ∘ natDegree) t) = (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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ t.prod.degree = (Multiset.map degree t).sum
have rw₄ : Multiset.sum (Multiset.map (fun (x : R[X]) ↦ (↑x.natDegree : WithBot ℕ)) t) = (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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ t.prod.degree = (Multiset.map degree t).sum
have rw₅ : (Multiset.map degree t).sum = (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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Multiset R[X]
n : ℕ
hl : ∀ p ∈ t, p.natDegree ≤ n
⊢ t.prod.coeff (t.card * n) = prod (Multiset.map (fun (p : R[X]) ↦ p.coeff n) t)
have 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⟧)
Tactic: induction t using Quotient.inductionOn
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
f : ι → R[X]
n : ℕ
h : ∀ p ∈ s, (f p).natDegree ≤ n
⊢ Eq.{u + 1} (α := R) (coeff (∏ i ∈ s, f i) (#s * n)) (∏ i ∈ s, (f i).coeff n)
have 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)
Tactic: obtain ⟨l, hl⟩ := s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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.{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)
have h₁ : #{ val := l, nodup := hl : Finset ι } = (Multiset.map f l).card
Tactic: convert! coeff_multiset_prod_of_natDegree_le (l.map f) n ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ 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)
have 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)))
Tactic: convert! coeff_multiset_prod_of_natDegree_le (l.map f) n ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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)))
⊢ 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)
have convert! : ∀ p ∈ Multiset.map f l, p.natDegree ≤ n
Tactic: convert! coeff_multiset_prod_of_natDegree_le (l.map f) n ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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)
have refine_1 : Eq.{u + 1} (α := R) (coeff (prod 0) 0) (prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) 0))
Tactic: refine Multiset.induction_on t ?_ fun a t ht => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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))
⊢ t.prod.coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t)
have 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))
Tactic: refine Multiset.induction_on t ?_ fun a t ht => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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)
⊢ (a ::ₘ t).prod.coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) (a ::ₘ t))
have refine_2 : (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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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))
⊢ (a ::ₘ t).prod.coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) (a ::ₘ t))
have refine_2₁ : (a * t.prod).coeff 0 = (a.coeff 0 ::ₘ Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t).prod
Tactic: rw [Multiset.prod_cons, Multiset.map_cons, Multiset.prod_cons, Polynomial.mul_coeff_zero, ht]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ (a ::ₘ t).prod.coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) (a ::ₘ t))
have refine_2₂ : (a * t.prod).coeff 0 = a.coeff 0 * prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t)
Tactic: rw [Multiset.prod_cons, Multiset.map_cons, Multiset.prod_cons, Polynomial.mul_coeff_zero, ht]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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)
⊢ (a ::ₘ t).prod.coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) (a ::ₘ t))
have refine_2₃ : a.coeff 0 * t.prod.coeff 0 = a.coeff 0 * prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) t)
Tactic: rw [Multiset.prod_cons, Multiset.map_cons, Multiset.prod_cons, Polynomial.mul_coeff_zero, ht]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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)
⊢ (a ::ₘ t).prod.coeff 0 = prod (Multiset.map (fun (f : R[X]) ↦ f.coeff 0) (a ::ₘ t))
have 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)
Tactic: rw [Multiset.prod_cons, Multiset.map_cons, Multiset.prod_cons, Polynomial.mul_coeff_zero, ht]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
t : Multiset R
⊢ 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
have 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
Tactic: rw [nextCoeff_multiset_prod]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ 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
have h : ∀ i ∈ t, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).Monic
Tactic: rw [nextCoeff_multiset_prod]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
t : Multiset R
⊢ 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
have simp : Multiset.sum (Multiset.map (fun (x : R) ↦ -x) t) = -t.sum
Tactic: simp only [nextCoeff_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (hypothesis)
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
⊢ 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
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial 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) =
    -t.sum
have 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)))
Tactic: convert! multiset_prod_X_sub_C_nextCoeff (by assumption)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial R
⊢ 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)))
have 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))
Tactic: rw [nextCoeff, if_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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))
⊢ 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)))
have 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
Tactic: rw [nextCoeff, if_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial R
⊢ ¬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
have 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
Tactic: rw [natDegree_multiset_prod_of_monic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ ¬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
have 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
Tactic: rw [natDegree_multiset_prod_of_monic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
have h : ∀ (f : R[X]), (∃ a ∈ t, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = f) → f.Monic
Tactic: simp only [Multiset.mem_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial R
⊢ ¬(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
have 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
Tactic: simp_rw [Multiset.sum_eq_zero_iff, Multiset.mem_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial R
⊢ ¬∀ (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
have 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
Tactic: obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp ht
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial R
⊢ 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))
have 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))
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
t : Multiset R
ht : 0 < t.card
h : Nontrivial R
⊢ 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))
have 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
Tactic: rw [natDegree_multiset_prod_of_monic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ 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))
have 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
Tactic: rw [natDegree_multiset_prod_of_monic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
have 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
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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
⊢ 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
have 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)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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 ι)
⊢ (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)))
have a : ∀ b ∈ s, (f b).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
Tactic: apply Finset.sup_le
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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 ι)
i : ι
hi : i ∈ s
⊢ (f i).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
have pos : ∀ (hf : f i = 0),
  (f i).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
Tactic: by_cases hf : f i = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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 ι)
i : ι
hi : i ∈ s
pos :
  ∀ (hf : f i = 0),
    (f i).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
⊢ (f i).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
have neg : ∀ (hf : ¬f i = 0),
  (f i).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
Tactic: by_cases hf : f i = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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 ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ (f i).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
have neg : (↑(f i).natDegree : WithBot ℕ) ≤
  degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
Tactic: rw [degree_eq_natDegree hf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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 ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ (↑(f i).natDegree : WithBot ℕ) ≤
    degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
have neg : Ne.{u_1 + 1} (α := A) (coeff (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) (f i).natDegree) 0
Tactic: apply le_degree_of_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
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 ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ Ne.{u_1 + 1} (α := A) (coeff (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) (f i).natDegree) 0
have neg : Ne.{u_1 + 1} (α := A) (∑ b ∈ s, (HSMul.hSMul (β := A[X]) (v b) (map (algebraMap R A) (f b))).coeff (f i).natDegree) 0
Tactic: rw [finsetSum_coeff]