α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
⊢ ∃ p, a ~ᵤ p ∧ f = {p}
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
⊢ ∃ p, a ~ᵤ p ∧ f = {p}
haveI := Classical.decEq α
case refine_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
⊢ (fun g => Multiset.prod g ~ᵤ a → (∀ (b : α), b ∈ g → Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) 0

case refine_2
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
⊢ ∀ ⦃a_1 : α⦄ {s : Multiset α},
    (fun g => Multiset.prod g ~ᵤ a → (∀ (b : α), b ∈ g → Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) s →
      (fun g => Multiset.prod g ~ᵤ a → (∀ (b : α), b ∈ g → Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) (a_1 ::ₘ s)
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
⊢ ∃ p, a ~ᵤ p ∧ f = {p}
refine @Multiset.induction_on _
  (fun g => (g.prod ~ᵤ a) → (∀ b ∈ g, Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) f ?_ ?_ pfa.2 pfa.1
case refine_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
h : Multiset.prod 0 ~ᵤ a
⊢ (∀ (b : α), b ∈ 0 → Prime b) → ∃ p, a ~ᵤ p ∧ 0 = {p}
case refine_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
⊢ (fun g => Multiset.prod g ~ᵤ a → (∀ (b : α), b ∈ g → Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) 0
intro h
no goals
case refine_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
h : Multiset.prod 0 ~ᵤ a
⊢ (∀ (b : α), b ∈ 0 → Prime b) → ∃ p, a ~ᵤ p ∧ 0 = {p}
exact (ha.not_unit (associated_one_iff_isUnit.1 (Associated.symm h))).elim
case refine_2.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
⊢ ∃ p_1, a ~ᵤ p_1 ∧ p ::ₘ s = {p_1}
case refine_2
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
⊢ ∀ ⦃a_1 : α⦄ {s : Multiset α},
    (fun g => Multiset.prod g ~ᵤ a → (∀ (b : α), b ∈ g → Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) s →
      (fun g => Multiset.prod g ~ᵤ a → (∀ (b : α), b ∈ g → Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) (a_1 ::ₘ s)
rintro p s _ ⟨u, hu⟩ hs
case refine_2.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
⊢ a ~ᵤ p ∧ p ::ₘ s = {p}
case refine_2.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
⊢ ∃ p_1, a ~ᵤ p_1 ∧ p ::ₘ s = {p_1}
use p
case refine_2.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
u : αˣ
a✝ : 1 ~ᵤ a → (∀ (b : α), b ∈ 0 → Prime b) → ∃ p, a ~ᵤ p ∧ 0 = {p}
hu : p * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ 0 → Prime b
hs0 : True
⊢ a ~ᵤ p ∧ p ::ₘ 0 = {p}
case refine_2.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : s = 0
⊢ a ~ᵤ p ∧ p ::ₘ s = {p}
simp only [mul_one, Multiset.prod_cons, Multiset.prod_zero, hs0] at *
no goals
case refine_2.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
u : αˣ
a✝ : 1 ~ᵤ a → (∀ (b : α), b ∈ 0 → Prime b) → ∃ p, a ~ᵤ p ∧ 0 = {p}
hu : p * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ 0 → Prime b
hs0 : True
⊢ a ~ᵤ p ∧ p ::ₘ 0 = {p}
exact ⟨Associated.symm ⟨u, hu⟩, rfl⟩
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
⊢ False
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
⊢ s = 0
by_contra hs0
case intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ False
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
⊢ False
obtain ⟨q, hq⟩ := Multiset.exists_mem_of_ne_zero hs0
case intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ IsUnit q
case intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ False
apply (hs q (by simp [hq])).2.1
case intro.refine'_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ a = p * ↑u * Multiset.prod (Multiset.erase s q) * q

case intro.refine'_2
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ ¬IsUnit (p * ↑u * Multiset.prod (Multiset.erase s q))
case intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ IsUnit q
refine' (ha.isUnit_or_isUnit (_ : _ = p * ↑u * (s.erase q).prod * _)).resolve_left _
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ ¬IsUnit p
case intro.refine'_2
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ ¬IsUnit (p * ↑u * Multiset.prod (Multiset.erase s q))
apply mt isUnit_of_mul_isUnit_left (mt isUnit_of_mul_isUnit_left _)
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ ¬IsUnit p
apply (hs p (Multiset.mem_cons_self _ _)).2.1
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ q ∈ p ::ₘ s
simp [hq]
case intro.refine'_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ ↑u * Multiset.prod (p ::ₘ s) = ↑u * (p * Multiset.prod s)
case intro.refine'_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ a = p * ↑u * Multiset.prod (Multiset.erase s q) * q
rw [mul_right_comm _ _ q, mul_assoc, ← Multiset.prod_cons, Multiset.cons_erase hq, ← hu,
  mul_comm, mul_comm p _, mul_assoc]
no goals
case intro.refine'_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : Multiset.prod s ~ᵤ a → (∀ (b : α), b ∈ s → Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : Multiset.prod (p ::ₘ s) * ↑u = a
hs : ∀ (b : α), b ∈ p ::ₘ s → Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ ↑u * Multiset.prod (p ::ₘ s) = ↑u * (p * Multiset.prod s)
simp