no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : a * b = 0
ha0 : a = 0
⊢ p ∣ a ∨ p ∣ b
simp [ha0]
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : a * b = 0
hb0 : b = 0
⊢ p ∣ a ∨ p ∣ b
simp [hb0]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
⊢ p ∣ a ∨ p ∣ b
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
⊢ p ∣ a ∨ p ∣ b
have hx0 : x ≠ 0 := fun hx0 => by simp_all
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
⊢ p ∣ a ∨ p ∣ b
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
⊢ p ∣ a ∨ p ∣ b
have ha0 : a ≠ 0 := left_ne_zero_of_mul hab0
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ p ∣ a ∨ p ∣ b
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
⊢ p ∣ a ∨ p ∣ b
have hb0 : b ≠ 0 := right_ne_zero_of_mul hab0
case intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
⊢ p ∣ a ∨ p ∣ b
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ p ∣ a ∨ p ∣ b
cases' eif x hx0 with fx hfx
case intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
⊢ p ∣ a ∨ p ∣ b
case intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
⊢ p ∣ a ∨ p ∣ b
cases' eif a ha0 with fa hfa
case intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
⊢ p ∣ a ∨ p ∣ b
case intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
⊢ p ∣ a ∨ p ∣ b
cases' eif b hb0 with fb hfb
no goals
case intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
h : Multiset.Rel Associated (p ::ₘ fx) (fa + fb)
⊢ p ∣ a ∨ p ∣ b
exact
  let ⟨q, hqf, hq⟩ := Multiset.exists_mem_of_rel_of_mem h (Multiset.mem_cons_self p _)
  (Multiset.mem_add.1 hqf).elim
    (fun hqa =>
      Or.inl <| hq.dvd_iff_dvd_left.2 <| hfa.2.dvd_iff_dvd_right.1 (Multiset.dvd_prod hqa))
    fun hqb =>
    Or.inr <| hq.dvd_iff_dvd_left.2 <| hfb.2.dvd_iff_dvd_right.1 (Multiset.dvd_prod hqb)
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x = 0
⊢ False
simp_all
case a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
⊢ ∀ (x : α), x ∈ p ::ₘ fx → Irreducible x

case a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
⊢ ∀ (x : α), x ∈ fa + fb → Irreducible x

case a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
⊢ Multiset.prod (p ::ₘ fx) ~ᵤ Multiset.prod (fa + fb)
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
⊢ Multiset.Rel Associated (p ::ₘ fx) (fa + fb)
apply uif
no goals
case a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
⊢ Multiset.prod (p ::ₘ fx) ~ᵤ Multiset.prod (fa + fb)
calc
  Multiset.prod (p ::ₘ fx) ~ᵤ a * b := by
    rw [hx, Multiset.prod_cons]; exact hfx.2.mul_left _
  _ ~ᵤ fa.prod * fb.prod := (hfa.2.symm.mul_mul hfb.2.symm)
  _ = _ := by rw [Multiset.prod_add]
no goals
case a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
⊢ ∀ (x : α), x ∈ p ::ₘ fx → Irreducible x
exact fun i hi => (Multiset.mem_cons.1 hi).elim (fun hip => hip.symm ▸ hpi) (hfx.1 _)
no goals
case a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
⊢ ∀ (x : α), x ∈ fa + fb → Irreducible x
exact fun i hi => (Multiset.mem_add.1 hi).elim (hfa.1 _) (hfb.1 _)
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
⊢ p * Multiset.prod fx ~ᵤ p * x
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
⊢ Multiset.prod (p ::ₘ fx) ~ᵤ a * b
rw [hx, Multiset.prod_cons]
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
⊢ p * Multiset.prod fx ~ᵤ p * x
exact hfx.2.mul_left _
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ (x : α), x ∈ f → Irreducible x) →
      (∀ (x : α), x ∈ g → Irreducible x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ (b : α), b ∈ fx → Irreducible b) ∧ Multiset.prod fx ~ᵤ x
fa : Multiset α
hfa : (∀ (b : α), b ∈ fa → Irreducible b) ∧ Multiset.prod fa ~ᵤ a
fb : Multiset α
hfb : (∀ (b : α), b ∈ fb → Irreducible b) ∧ Multiset.prod fb ~ᵤ b
⊢ Multiset.prod fa * Multiset.prod fb = Multiset.prod (fa + fb)
rw [Multiset.prod_add]