-- Mathlib/Algebra/BigOperators/Associated.lean
theorem exists_associated_mem_of_dvd_prod [CancelCommMonoidWithZero α] {p : α} (hp : Prime p)
    {s : Multiset α} : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q :=
  Multiset.induction_on s (by simp [mt isUnit_iff_dvd_one.2 hp.not_unit]) fun a s ih hs hps => by
    rw [Multiset.prod_cons] at hps
    rcases hp.dvd_or_dvd hps with h | h
    · have hap := hs a (Multiset.mem_cons.2 (Or.inl rfl))
      exact ⟨a, Multiset.mem_cons_self a _, hp.associated_of_dvd hap h⟩
    · rcases ih (fun r hr => hs _ (Multiset.mem_cons.2 (Or.inr hr))) h with ⟨q, hq₁, hq₂⟩
      exact ⟨q, Multiset.mem_cons.2 (Or.inr hq₁), hq₂⟩

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s : Multiset α
⊢ (∀ r ∈ 0, Prime r) → p ∣ Multiset.prod 0 → ∃ q ∈ 0, p ~ᵤ q

Tactic:
simp [mt isUnit_iff_dvd_one.2 hp.not_unit]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ (a ::ₘ s).prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
rw [Multiset.prod_cons] at hps

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Proof state:
case inr.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ s.prod
q : α
hq₁ : q ∈ s
hq₂ : p ~ᵤ q
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
exact ⟨q, Multiset.mem_cons.2 (Or.inr hq₁), hq₂⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
rcases hp.dvd_or_dvd hps with h | h

Result:
case inl
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ a
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

case inr
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Proof state:
case inl
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ a
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
have hap := hs a (Multiset.mem_cons.2 (Or.inl rfl))

Result:
case inl
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ a
hap : Prime a
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Proof state:
case inl
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ a
hap : Prime a
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
exact ⟨a, Multiset.mem_cons_self a _, hp.associated_of_dvd hap h⟩

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
rcases ih (fun r hr => hs _ (Multiset.mem_cons.2 (Or.inr hr))) h with ⟨q, hq₁, hq₂⟩

Result:
case inr.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ s.prod
q : α
hq₁ : q ∈ s
hq₂ : p ~ᵤ q
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q