[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : p ∣ Multiset.prod s → ∃ a, a ∈ s ∧ p ∣ a
h : p ∣ Multiset.prod (a ::ₘ s)
⊢ p ∣ a * Multiset.prod s
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp : Prime p
s : Multiset β
f : β → α
h : p ∣ Multiset.prod (Multiset.map f s)
⊢ ∃ a, a ∈ s ∧ p ∣ f a
[PROOFSTEP]
simpa only [exists_prop, Multiset.mem_map, exists_exists_and_eq_and] using hp.exists_mem_multiset_dvd h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s : Multiset α
⊢ (∀ (r : α), r ∈ 0 → Prime r) → p ∣ Multiset.prod 0 → ∃ q, q ∈ 0 ∧ p ~ᵤ q
[PROOFSTEP]
simp [mt isUnit_iff_dvd_one.2 hp.not_unit]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
[PROOFSTEP]
rw [Multiset.prod_cons] at hps 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
[PROOFSTEP]
cases' hp.dvd_or_dvd hps with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
[PROOFSTEP]
have hap := hs a (Multiset.mem_cons.2 (Or.inl rfl))
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
[PROOFSTEP]
exact ⟨a, Multiset.mem_cons_self a _, hp.associated_of_dvd hap h⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
[PROOFSTEP]
rcases ih (fun r hr => hs _ (Multiset.mem_cons.2 (Or.inr hr))) h with ⟨q, hq₁, hq₂⟩
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
[PROOFSTEP]
exact ⟨q, Multiset.mem_cons.2 (Or.inr hq₁), hq₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s : Multiset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
uniq : ∀ (a : α), countp (Associated a) s ≤ 1
⊢ prod s ∣ n
[PROOFSTEP]
induction' s using Multiset.induction_on with a s induct n primes divs generalizing n
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s : Multiset α
n✝ : α
h✝ : ∀ (a : α), a ∈ s → Prime a
div✝ : ∀ (a : α), a ∈ s → a ∣ n✝
uniq✝ : ∀ (a : α), countp (Associated a) s ≤ 1
n : α
h : ∀ (a : α), a ∈ 0 → Prime a
div : ∀ (a : α), a ∈ 0 → a ∣ n
uniq : ∀ (a : α), countp (Associated a) 0 ≤ 1
⊢ prod 0 ∣ n
[PROOFSTEP]
simp only [Multiset.prod_zero, one_dvd]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n✝ : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n✝
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
n : α
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ n
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
⊢ prod (a ::ₘ s) ∣ n
[PROOFSTEP]
rw [Multiset.prod_cons]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n✝ : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n✝
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
n : α
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ n
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
⊢ a * prod s ∣ n
[PROOFSTEP]
obtain ⟨k, rfl⟩ : a ∣ n := div a (Multiset.mem_cons_self a s)
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
⊢ a * prod s ∣ a * k
[PROOFSTEP]
apply mul_dvd_mul_left a
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
⊢ prod s ∣ k
[PROOFSTEP]
refine
  induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_) fun a =>
    (Multiset.countp_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
⊢ b ∣ k
[PROOFSTEP]
have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
⊢ b ∣ k
[PROOFSTEP]
have a_prime := h a (Multiset.mem_cons_self a s)
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
⊢ b ∣ k
[PROOFSTEP]
have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
⊢ b ∣ k
[PROOFSTEP]
refine' (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => _
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
⊢ False
[PROOFSTEP]
have assoc := b_prime.associated_of_dvd a_prime b_div_a
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
⊢ False
[PROOFSTEP]
have := uniq a
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
this : countp (Associated a) (a ::ₘ s) ≤ 1
⊢ False
[PROOFSTEP]
rw [Multiset.countp_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt, Multiset.countp_pos] at this 
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
this : ¬∃ a_1, a_1 ∈ s ∧ a ~ᵤ a_1
⊢ False
[PROOFSTEP]
exact this ⟨b, b_in_s, assoc.symm⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∏ p in s, p ∣ n
[PROOFSTEP]
classical exact
  Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
    (by simpa only [Multiset.map_id', Finset.mem_def] using div)
    (by
      -- POrting note: was
                -- `simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter, ←
                --    Multiset.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup]`
      intro a
      simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter]
      change Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
      apply le_of_eq_of_le (Multiset.count_eq_card_filter_eq _ _).symm
      apply Multiset.nodup_iff_count_le_one.mp
      exact s.nodup)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∏ p in s, p ∣ n
[PROOFSTEP]
exact
  Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
    (by simpa only [Multiset.map_id', Finset.mem_def] using div)
    (by
      -- POrting note: was
                -- `simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter, ←
                --    Multiset.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup]`
      intro a
      simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter]
      change Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
      apply le_of_eq_of_le (Multiset.count_eq_card_filter_eq _ _).symm
      apply Multiset.nodup_iff_count_le_one.mp
      exact s.nodup)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∀ (a : α), a ∈ Multiset.map (fun p => p) s.val → Prime a
[PROOFSTEP]
simpa only [Multiset.map_id', Finset.mem_def] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∀ (a : α), a ∈ Multiset.map (fun p => p) s.val → a ∣ n
[PROOFSTEP]
simpa only [Multiset.map_id', Finset.mem_def] using div
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∀ (a : α), Multiset.countp (Associated a) (Multiset.map (fun p => p) s.val) ≤ 1
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ Multiset.countp (Associated a) (Multiset.map (fun p => p) s.val) ≤ 1
[PROOFSTEP]
simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ ↑Multiset.card (Multiset.filter (Eq a) s.val) ≤ 1
[PROOFSTEP]
change Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ ↑Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
[PROOFSTEP]
apply le_of_eq_of_le (Multiset.count_eq_card_filter_eq _ _).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ Multiset.count a s.val ≤ 1
[PROOFSTEP]
apply Multiset.nodup_iff_count_le_one.mp
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ Multiset.Nodup s.val
[PROOFSTEP]
exact s.nodup
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p : Multiset α
⊢ Multiset.prod (Multiset.map Associates.mk 0) = Associates.mk (Multiset.prod 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p : Multiset α
a : α
s : Multiset α
ih : Multiset.prod (Multiset.map Associates.mk s) = Associates.mk (Multiset.prod s)
⊢ Multiset.prod (Multiset.map Associates.mk (a ::ₘ s)) = Associates.mk (Multiset.prod (a ::ₘ s))
[PROOFSTEP]
simp [ih, Associates.mk_mul_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p : Finset β
f : β → α
⊢ ∏ i in p, Associates.mk (f i) = Associates.mk (∏ i in p, f i)
[PROOFSTEP]
have : (fun i => Associates.mk (f i)) = Associates.mk ∘ f := funext <| fun x => Function.comp_apply
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p : Finset β
f : β → α
this : (fun i => Associates.mk (f i)) = Associates.mk ∘ f
⊢ ∏ i in p, Associates.mk (f i) = Associates.mk (∏ i in p, f i)
[PROOFSTEP]
rw [Finset.prod_eq_multiset_prod, this, ← Multiset.map_map, prod_mk, ← Finset.prod_eq_multiset_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset α
⊢ Multiset.Rel Associated p q ↔ Multiset.map Associates.mk p = Multiset.map Associates.mk q
[PROOFSTEP]
rw [← Multiset.rel_eq, Multiset.rel_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset α
⊢ Multiset.Rel Associated p q ↔ Multiset.Rel (fun a b => Associates.mk a = Associates.mk b) p q
[PROOFSTEP]
simp only [mk_eq_mk_iff_associated]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p : Multiset (Associates α)
⊢ Multiset.prod 0 = 1 ↔ ∀ (a : Associates α), a ∈ 0 → a = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p : Multiset (Associates α)
⊢ ∀ ⦃a : Associates α⦄ {s : Multiset (Associates α)},
    (Multiset.prod s = 1 ↔ ∀ (a : Associates α), a ∈ s → a = 1) →
      (Multiset.prod (a ::ₘ s) = 1 ↔ ∀ (a_2 : Associates α), a_2 ∈ a ::ₘ s → a_2 = 1)
[PROOFSTEP]
simp (config := { contextual := true }) [mul_eq_one_iff, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
⊢ Multiset.prod p ≤ Multiset.prod q
[PROOFSTEP]
haveI := Classical.decEq (Associates α)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this : DecidableEq (Associates α)
⊢ Multiset.prod p ≤ Multiset.prod q
[PROOFSTEP]
haveI := Classical.decEq α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ Multiset.prod p ≤ Multiset.prod q
[PROOFSTEP]
suffices p.prod ≤ (p + (q - p)).prod by rwa [add_tsub_cancel_of_le h] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝¹ : DecidableEq (Associates α)
this✝ : DecidableEq α
this : Multiset.prod p ≤ Multiset.prod (p + (q - p))
⊢ Multiset.prod p ≤ Multiset.prod q
[PROOFSTEP]
rwa [add_tsub_cancel_of_le h] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ Multiset.prod p ≤ Multiset.prod (p + (q - p))
[PROOFSTEP]
suffices p.prod * 1 ≤ p.prod * (q - p).prod by simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝¹ : DecidableEq (Associates α)
this✝ : DecidableEq α
this : Multiset.prod p * 1 ≤ Multiset.prod p * Multiset.prod (q - p)
⊢ Multiset.prod p ≤ Multiset.prod (p + (q - p))
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ Multiset.prod p * 1 ≤ Multiset.prod p * Multiset.prod (q - p)
[PROOFSTEP]
exact mul_mono (le_refl p.prod) one_le
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
s✝ : Multiset (Associates α)
p : Associates α
hp : Prime p
a : Associates α
s : Multiset (Associates α)
ih : p ≤ Multiset.prod s → ∃ a, a ∈ s ∧ p ≤ a
h : p ≤ Multiset.prod (a ::ₘ s)
⊢ p ≤ a * Multiset.prod s
[PROOFSTEP]
simpa using h
