-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem natDegree_multiset_prod_of_monic (h : ∀ f ∈ t, Monic f) :
    t.prod.natDegree = (t.map natDegree).sum

Proof state:
case h.e'_2.h.e'_3
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ ∀ b ∈ Multiset.map (fun f => f.leadingCoeff) t, b = 1

Tactic:
rintro i hi

Result:
case h.e'_2.h.e'_3
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
i : R
hi : i ∈ Multiset.map (fun f => f.leadingCoeff) t
⊢ i = 1

Proof state:
case h
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0

Tactic:
suffices (t.map fun f => leadingCoeff f).prod = 1 by
  rw [this]
  simp

Result:
case h
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ (Multiset.map (fun f => f.leadingCoeff) t).prod = 1

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
this : (Multiset.map (fun f => f.leadingCoeff) t).prod = 1
⊢ 1 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Tactic:
apply natDegree_multiset_prod'

Result:
case h
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Proof state:
case h
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ (Multiset.map (fun f => f.leadingCoeff) t).prod = 1

Tactic:
convert prod_replicate (Multiset.card t) (1 : R)

Result:
case h.e'_2.h.e'_3
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ Multiset.map (fun f => f.leadingCoeff) t = replicate t.card 1

case h.e'_3
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ 1 = 1 ^ t.card

Proof state:
case h.e'_2.h.e'_3.intro.intro
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
i : R[X]
hi✝ : i ∈ t
hi : i.leadingCoeff ∈ Multiset.map (fun f => f.leadingCoeff) t
⊢ i.leadingCoeff = 1

Tactic:
apply h

Result:
case h.e'_2.h.e'_3.intro.intro.a
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
i : R[X]
hi✝ : i ∈ t
hi : i.leadingCoeff ∈ Multiset.map (fun f => f.leadingCoeff) t
⊢ i ∈ t

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
this : (Multiset.map (fun f => f.leadingCoeff) t).prod = 1
⊢ (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0

Tactic:
rw [this]

Result:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
this : (Multiset.map (fun f => f.leadingCoeff) t).prod = 1
⊢ 1 ≠ 0

Proof state:
case h.e'_2.h.e'_3
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ Multiset.map (fun f => f.leadingCoeff) t = replicate t.card 1

Tactic:
simp only [eq_replicate, Multiset.card_map, eq_self_iff_true, true_and]

Result:
case h.e'_2.h.e'_3
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ ∀ b ∈ Multiset.map (fun f => f.leadingCoeff) t, b = 1

Proof state:
case h.e'_2.h.e'_3
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
i : R
hi : i ∈ Multiset.map (fun f => f.leadingCoeff) t
⊢ i = 1

Tactic:
obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp hi

Result:
case h.e'_2.h.e'_3.intro.intro
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
i : R[X]
hi✝ : i ∈ t
hi : i.leadingCoeff ∈ Multiset.map (fun f => f.leadingCoeff) t
⊢ i.leadingCoeff = 1

Proof state:
case h.e'_2.h.e'_3.intro.intro.a
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
i : R[X]
hi✝ : i ∈ t
hi : i.leadingCoeff ∈ Multiset.map (fun f => f.leadingCoeff) t
⊢ i ∈ t

Tactic:
assumption

Result:
no goals

Proof state:
case h.e'_3
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ 1 = 1 ^ t.card

Tactic:
simp

Result:
no goals