α : Type u_1
inst✝ : CancelCommMonoidWithZero α
f : Multiset α
⊢ ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
⊢ ∀ {f g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
intro f
case empty
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
⊢ ∀ {g : Multiset α},
    (∀ (x : α), x ∈ 0 → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod 0 ~ᵤ Multiset.prod g → Multiset.Rel Associated 0 g

case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
⊢ ∀ {g : Multiset α},
    (∀ (x : α), x ∈ p ::ₘ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g → Multiset.Rel Associated (p ::ₘ f) g
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
f : Multiset α
⊢ ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
induction' f using Multiset.induction_on with p f ih
case empty
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
g : Multiset α
a✝ : ∀ (x : α), x ∈ 0 → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
h : Multiset.prod 0 ~ᵤ Multiset.prod g
⊢ Multiset.Rel Associated 0 g
case empty
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
⊢ ∀ {g : Multiset α},
    (∀ (x : α), x ∈ 0 → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod 0 ~ᵤ Multiset.prod g → Multiset.Rel Associated 0 g
intros g _ hg h
no goals
case empty
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
g : Multiset α
a✝ : ∀ (x : α), x ∈ 0 → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
h : Multiset.prod 0 ~ᵤ Multiset.prod g
⊢ Multiset.Rel Associated 0 g
exact Multiset.rel_zero_left.2 <|
  Multiset.eq_zero_of_forall_not_mem fun x hx =>
    have : IsUnit g.prod := by simpa [associated_one_iff_isUnit] using h.symm
    (hg x hx).not_unit <|
      isUnit_iff_dvd_one.2 <| (Multiset.dvd_prod hx).trans (isUnit_iff_dvd_one.1 this)
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
g : Multiset α
a✝ : ∀ (x : α), x ∈ 0 → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
h : Multiset.prod 0 ~ᵤ Multiset.prod g
x : α
hx : x ∈ g
⊢ IsUnit (Multiset.prod g)
simpa [associated_one_iff_isUnit] using h.symm
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
⊢ Multiset.Rel Associated (p ::ₘ f) g
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
⊢ ∀ {g : Multiset α},
    (∀ (x : α), x ∈ p ::ₘ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g → Multiset.Rel Associated (p ::ₘ f) g
intros g hf hg hfg
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
b : α
hbg : b ∈ g
hb : p ~ᵤ b
⊢ Multiset.Rel Associated (p ::ₘ f) g
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
⊢ Multiset.Rel Associated (p ::ₘ f) g
let ⟨b, hbg, hb⟩ :=
  (exists_associated_mem_of_dvd_prod (hf p (by simp)) fun q hq => hg _ hq) <|
    hfg.dvd_iff_dvd_right.1 (show p ∣ (p ::ₘ f).prod by simp)
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ Multiset.Rel Associated (p ::ₘ f) g
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
b : α
hbg : b ∈ g
hb : p ~ᵤ b
⊢ Multiset.Rel Associated (p ::ₘ f) g
haveI := Classical.decEq α
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ Multiset.Rel Associated (p ::ₘ f) (b ::ₘ Multiset.erase g b)
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ Multiset.Rel Associated (p ::ₘ f) g
rw [← Multiset.cons_erase hbg]
no goals
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ Multiset.Rel Associated (p ::ₘ f) (b ::ₘ Multiset.erase g b)
exact
  Multiset.Rel.cons hb
    (ih (fun q hq => hf _ (by simp [hq]))
      (fun {q} (hq : q ∈ g.erase b) => hg q (Multiset.mem_of_mem_erase hq))
      (Associated.of_mul_left
        (by rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]) hb
        (hf p (by simp)).ne_zero))
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
⊢ p ∈ p ::ₘ f
simp
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
⊢ p ∣ Multiset.prod (p ::ₘ f)
simp
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
q : α
hq : q ∈ f
⊢ q ∈ p ::ₘ f
simp [hq]
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ p * Multiset.prod f ~ᵤ b * Multiset.prod (Multiset.erase g b)
rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih :
  ∀ {g : Multiset α},
    (∀ (x : α), x ∈ f → Prime x) →
      (∀ (x : α), x ∈ g → Prime x) → Multiset.prod f ~ᵤ Multiset.prod g → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ (x : α), x ∈ p ::ₘ f → Prime x
hg : ∀ (x : α), x ∈ g → Prime x
hfg : Multiset.prod (p ::ₘ f) ~ᵤ Multiset.prod g
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ p ∈ p ::ₘ f
simp