no goals
α : Type u_1
β : Type ?u.13323
γ : Type ?u.13326
δ : Type ?u.13329
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s : Multiset α
⊢ (∀ (r : α), r ∈ 0 → Prime r) → p ∣ Multiset.prod 0 → ∃ q, q ∈ 0 ∧ p ~ᵤ q
simp [mt isUnit_iff_dvd_one.2 hp.not_unit]
α : Type u_1
β : Type ?u.13323
γ : Type ?u.13326
δ : Type ?u.13329
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
α : Type u_1
β : Type ?u.13323
γ : Type ?u.13326
δ : Type ?u.13329
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ Multiset.prod (a ::ₘ s)
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
rw [Multiset.prod_cons] at hps
case inl
α : Type u_1
β : Type ?u.13323
γ : Type ?u.13326
δ : Type ?u.13329
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
h : p ∣ a
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q

case inr
α : Type u_1
β : Type ?u.13323
γ : Type ?u.13326
δ : Type ?u.13329
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
h : p ∣ Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
α : Type u_1
β : Type ?u.13323
γ : Type ?u.13326
δ : Type ?u.13329
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
cases' hp.dvd_or_dvd hps with h h
case inl
α : Type u_1
β : Type ?u.13323
γ : Type ?u.13326
δ : Type ?u.13329
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
h : p ∣ a
hap : Prime a
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
case inl
α : Type u_1
β : Type ?u.13323
γ : Type ?u.13326
δ : Type ?u.13329
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
h : p ∣ a
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
have hap := hs a (Multiset.mem_cons.2 (Or.inl rfl))
no goals
case inl
α : Type u_1
β : Type ?u.13323
γ : Type ?u.13326
δ : Type ?u.13329
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
h : p ∣ a
hap : Prime a
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
exact ⟨a, Multiset.mem_cons_self a _, hp.associated_of_dvd hap h⟩
case inr.intro.intro
α : Type u_1
β : Type ?u.13323
γ : Type ?u.13326
δ : Type ?u.13329
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
h : p ∣ Multiset.prod s
q : α
hq₁ : q ∈ s
hq₂ : p ~ᵤ q
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
case inr
α : Type u_1
β : Type ?u.13323
γ : Type ?u.13326
δ : Type ?u.13329
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
h : p ∣ Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
rcases ih (fun r hr => hs _ (Multiset.mem_cons.2 (Or.inr hr))) h with ⟨q, hq₁, hq₂⟩
no goals
case inr.intro.intro
α : Type u_1
β : Type ?u.13323
γ : Type ?u.13326
δ : Type ?u.13329
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
h : p ∣ Multiset.prod s
q : α
hq₁ : q ∈ s
hq₂ : p ~ᵤ q
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
exact ⟨q, Multiset.mem_cons.2 (Or.inr hq₁), hq₂⟩