-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.nextCoeff_multiset_prod (t : Multiset ι) (f : ι → R[X]) (h : ∀ i ∈ t, Monic (f i)) :
    nextCoeff (t.map f).prod = (t.map fun i => nextCoeff (f i)).sum

Proof state:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) (a ::ₘ t)).sum

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons,
  Monic.nextCoeff_mul, ih]

Result:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ ∀ i ∈ t, (f i).Monic

case refine_2.hp
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a).Monic

case refine_2.hq
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f t).prod.Monic

Proof state:
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum

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

Result:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ 0, (f i).Monic) → (Multiset.map f 0).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) 0).sum

case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) (a ::ₘ t)).sum

Proof state:
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
h : ∀ i ∈ t, (f i).Monic
⊢ (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum

Tactic:
revert h

Result:
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum

Proof state:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ ∀ i ∈ t, (f i).Monic

case refine_2.hp
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a).Monic

case refine_2.hq
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f t).prod.Monic

Tactic:
exacts [fun i hi => ht i (Multiset.mem_cons_of_mem hi), ht a (Multiset.mem_cons_self _ _),
  monic_multiset_prod_of_monic _ _ fun b bs => ht _ (Multiset.mem_cons_of_mem bs)]

Result:
no goals

Proof state:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (C 1).nextCoeff = 0

Tactic:
rw [nextCoeff_C_eq_zero]

Result:
no goals

Proof state:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ 0, (f i).Monic) → (Multiset.map f 0).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) 0).sum

Tactic:
simp only [Multiset.not_mem_zero, forall_prop_of_true, forall_prop_of_false, Multiset.map_zero,
  Multiset.prod_zero, Multiset.sum_zero, not_false_iff, forall_true_iff]

Result:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ nextCoeff 1 = 0

Proof state:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ nextCoeff 1 = 0

Tactic:
rw [← C_1]

Result:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (C 1).nextCoeff = 0