R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ natDegree (prod t) = Multiset.sum (Multiset.map natDegree t)
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
⊢ natDegree (prod t) = Multiset.sum (Multiset.map natDegree t)
nontriviality R
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ natDegree (prod t) = Multiset.sum (Multiset.map natDegree t)
apply natDegree_multiset_prod'
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ prod (Multiset.map (fun f => leadingCoeff f) t) = 1
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0
suffices (t.map fun f => leadingCoeff f).prod = 1 by
  rw [this]
  simp
case h.e'_2.h.e'_3
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ Multiset.map (fun f => leadingCoeff f) t = replicate (↑Multiset.card t) 1

case h.e'_3
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ 1 = 1 ^ ↑Multiset.card t
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ prod (Multiset.map (fun f => leadingCoeff f) t) = 1
convert prod_replicate (Multiset.card t) (1 : R)
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
this : prod (Multiset.map (fun f => leadingCoeff f) t) = 1
⊢ 1 ≠ 0
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
this : prod (Multiset.map (fun f => leadingCoeff f) t) = 1
⊢ prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0
rw [this]
no goals
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
this : prod (Multiset.map (fun f => leadingCoeff f) t) = 1
⊢ 1 ≠ 0
simp
case h.e'_2.h.e'_3
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ ∀ (b : R), b ∈ Multiset.map (fun f => leadingCoeff f) t → b = 1
case h.e'_2.h.e'_3
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ Multiset.map (fun f => leadingCoeff f) t = replicate (↑Multiset.card t) 1
simp only [eq_replicate, Multiset.card_map, eq_self_iff_true, true_and_iff]
case h.e'_2.h.e'_3
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
i : R
hi : i ∈ Multiset.map (fun f => leadingCoeff f) t
⊢ i = 1
case h.e'_2.h.e'_3
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ ∀ (b : R), b ∈ Multiset.map (fun f => leadingCoeff f) t → b = 1
rintro i hi
case h.e'_2.h.e'_3.intro.intro
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
i : R[X]
hi✝ : i ∈ t
hi : leadingCoeff i ∈ Multiset.map (fun f => leadingCoeff f) t
⊢ leadingCoeff i = 1
case h.e'_2.h.e'_3
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
i : R
hi : i ∈ Multiset.map (fun f => leadingCoeff f) t
⊢ i = 1
obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp hi
case h.e'_2.h.e'_3.intro.intro.a
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
i : R[X]
hi✝ : i ∈ t
hi : leadingCoeff i ∈ Multiset.map (fun f => leadingCoeff f) t
⊢ i ∈ t
case h.e'_2.h.e'_3.intro.intro
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
i : R[X]
hi✝ : i ∈ t
hi : leadingCoeff i ∈ Multiset.map (fun f => leadingCoeff f) t
⊢ leadingCoeff i = 1
apply h
no goals
case h.e'_2.h.e'_3.intro.intro.a
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
i : R[X]
hi✝ : i ∈ t
hi : leadingCoeff i ∈ Multiset.map (fun f => leadingCoeff f) t
⊢ i ∈ t
assumption
no goals
case h.e'_3
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ 1 = 1 ^ ↑Multiset.card t
simp