-- Mathlib/Algebra/BigOperators/Associated.lean
theorem Multiset.prod_primes_dvd [CancelCommMonoidWithZero α]
    [∀ a : α, DecidablePred (Associated a)] {s : Multiset α} (n : α) (h : ∀ a ∈ s, Prime a)
    (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ a, s.countP (Associated a) ≤ 1) : s.prod ∣ n

Proof state:
case cons.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ 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 ∈ s, a ~ᵤ a_1
⊢ False

Tactic:
exact this ⟨b, b_in_s, assoc.symm⟩

Result:
no goals

Proof state:
case cons.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ 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

Tactic:
have := uniq a

Result:
case cons.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ 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

Proof state:
case cons
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
n : α
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ n
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
⊢ (a ::ₘ s).prod ∣ n

Tactic:
rw [Multiset.prod_cons]

Result:
case cons
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
n : α
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ n
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
⊢ a * s.prod ∣ n

Proof state:
case cons.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : α
b_in_s : b ∈ s
⊢ b ∣ k

Tactic:
have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)

Result:
case cons.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
⊢ b ∣ k

Proof state:
case cons.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ 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

Tactic:
have assoc := b_prime.associated_of_dvd a_prime b_div_a

Result:
case cons.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ 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

Proof state:
case cons.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
⊢ a * s.prod ∣ a * k

Tactic:
apply mul_dvd_mul_left a

Result:
case cons.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
⊢ s.prod ∣ k

Proof state:
case empty
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
n : α
h : ∀ a ∈ 0, Prime a
div : ∀ a ∈ 0, a ∣ n
uniq : ∀ (a : α), countP (Associated a) 0 ≤ 1
⊢ prod 0 ∣ n

Tactic:
simp only [Multiset.prod_zero, one_dvd]

Result:
no goals

Proof state:
case cons.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ 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

Tactic:
rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
  Multiset.countP_pos] at this

Result:
case cons.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
a : α
s : Multiset α
induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ 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 ∈ s, a ~ᵤ a_1
⊢ False