-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem natDegree_multiset_prod' (h : (t.map fun f => leadingCoeff f).prod ≠ 0) :
    t.prod.natDegree = (t.map fun f => natDegree f).sum

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
ht : (Multiset.map (fun f => f.leadingCoeff) (a ::ₘ t)).prod ≠ 0
⊢ (a ::ₘ t).prod.natDegree = (Multiset.map (fun f => f.natDegree) (a ::ₘ t)).sum

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons] at ht ⊢

Result:
case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0
⊢ (a * t.prod).natDegree = (a.natDegree ::ₘ Multiset.map (fun f => f.natDegree) t).sum

Proof state:
case refine_2.h
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0
⊢ (Multiset.map leadingCoeff t).prod ≠ 0

Tactic:
apply right_ne_zero_of_mul ht

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0
⊢ t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum

Tactic:
revert h

Result:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0

Tactic:
rwa [Polynomial.leadingCoeff_multiset_prod']

Result:
case refine_2.h
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0
⊢ (Multiset.map leadingCoeff t).prod ≠ 0

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum

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

Result:
case refine_1
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (Multiset.map (fun f => f.leadingCoeff) 0).prod ≠ 0 → (prod 0).natDegree = (Multiset.map (fun f => f.natDegree) 0).sum

case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
ht : (Multiset.map (fun f => f.leadingCoeff) (a ::ₘ t)).prod ≠ 0
⊢ (a ::ₘ t).prod.natDegree = (Multiset.map (fun f => f.natDegree) (a ::ₘ t)).sum

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0
⊢ (a * t.prod).natDegree = (a.natDegree ::ₘ Multiset.map (fun f => f.natDegree) t).sum

Tactic:
rw [Multiset.sum_cons, Polynomial.natDegree_mul', ih]

Result:
case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0
⊢ (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0

case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0

Proof state:
case refine_1
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (Multiset.map (fun f => f.leadingCoeff) 0).prod ≠ 0 → (prod 0).natDegree = (Multiset.map (fun f => f.natDegree) 0).sum

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0
⊢ (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0

Tactic:
apply right_ne_zero_of_mul ht

Result:
no goals