α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a✝ a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
x✝ : i * a ≠ 0
s : Multiset α
hs : (∀ (b : α), b ∈ s → Irreducible b) ∧ Multiset.prod s ~ᵤ a
⊢ i * Multiset.prod s ~ᵤ i * a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a✝ a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
x✝ : i * a ≠ 0
s : Multiset α
hs : (∀ (b : α), b ∈ s → Irreducible b) ∧ Multiset.prod s ~ᵤ a
⊢ Multiset.prod (i ::ₘ s) ~ᵤ i * a
rw [s.prod_cons i]
no goals
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a✝ a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
x✝ : i * a ≠ 0
s : Multiset α
hs : (∀ (b : α), b ∈ s → Irreducible b) ∧ Multiset.prod s ~ᵤ a
⊢ i * Multiset.prod s ~ᵤ i * a
exact hs.2.mul_left i