[GOAL]
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ prod L ↔ ∃ a, a ∈ L ∧ p ∣ a
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ prod L → ∃ a, a ∈ L ∧ p ∣ a
[PROOFSTEP]
intro h
[GOAL]
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h : p ∣ prod L
⊢ ∃ a, a ∈ L ∧ p ∣ a
[PROOFSTEP]
induction' L with L_hd L_tl L_ih
[GOAL]
case mp.nil
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
h : p ∣ prod []
⊢ ∃ a, a ∈ [] ∧ p ∣ a
[PROOFSTEP]
rw [prod_nil] at h 
[GOAL]
case mp.nil
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
h : p ∣ 1
⊢ ∃ a, a ∈ [] ∧ p ∣ a
[PROOFSTEP]
exact absurd h pp.not_dvd_one
[GOAL]
case mp.cons
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
L_hd : M
L_tl : List M
L_ih : p ∣ prod L_tl → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ prod (L_hd :: L_tl)
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
[PROOFSTEP]
rw [prod_cons] at h 
[GOAL]
case mp.cons
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
L_hd : M
L_tl : List M
L_ih : p ∣ prod L_tl → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * prod L_tl
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
[PROOFSTEP]
cases' pp.dvd_or_dvd h with hd hd
[GOAL]
case mp.cons.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
L_hd : M
L_tl : List M
L_ih : p ∣ prod L_tl → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * prod L_tl
hd : p ∣ L_hd
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
[PROOFSTEP]
exact ⟨L_hd, mem_cons_self L_hd L_tl, hd⟩
[GOAL]
case mp.cons.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
L_hd : M
L_tl : List M
L_ih : p ∣ prod L_tl → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * prod L_tl
hd : p ∣ prod L_tl
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
[PROOFSTEP]
obtain ⟨x, hx1, hx2⟩ := L_ih hd
[GOAL]
case mp.cons.inr.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h✝ : p ∣ prod L
L_hd : M
L_tl : List M
L_ih : p ∣ prod L_tl → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * prod L_tl
hd : p ∣ prod L_tl
x : M
hx1 : x ∈ L_tl
hx2 : p ∣ x
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
[PROOFSTEP]
exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩
[GOAL]
case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ (∃ a, a ∈ L ∧ p ∣ a) → p ∣ prod L
[PROOFSTEP]
exact fun ⟨a, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod ha1)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ prod L
⊢ p ∈ L
[PROOFSTEP]
obtain ⟨x, hx1, hx2⟩ := hp.dvd_prod_iff.mp hpL
[GOAL]
case intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ prod L
x : M
hx1 : x ∈ L
hx2 : p ∣ x
⊢ p ∈ L
[PROOFSTEP]
rwa [(prime_dvd_prime_iff_eq hp (hL x hx1)).mp hx2]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
classical
have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
have ha : a ∈ b :: l₂ :=
  mem_list_primes_of_dvd_prod (hl₁ a (mem_cons_self _ _)) hl₂ (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
have hl : prod l₁ = prod ((b :: l₂).erase a) :=
  (mul_right_inj' (hl₁ a (mem_cons_self _ _)).ne_zero).1 <| by rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
have ha : a ∈ b :: l₂ :=
  mem_list_primes_of_dvd_prod (hl₁ a (mem_cons_self _ _)) hl₂ (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
⊢ a ∣ prod (a :: l₁)
[PROOFSTEP]
rw [prod_cons]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
⊢ a ∣ a * prod l₁
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: List.erase (b :: l₂) a
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
have hl : prod l₁ = prod ((b :: l₂).erase a) :=
  (mul_right_inj' (hl₁ a (mem_cons_self _ _)).ne_zero).1 <| by rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: List.erase (b :: l₂) a
⊢ a * prod l₁ = a * prod (List.erase (b :: l₂) a)
[PROOFSTEP]
rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : prod (a :: l₁) = prod (b :: l₂)
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ List.erase (b :: l₂) a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: List.erase (b :: l₂) a
hl : prod l₁ = prod (List.erase (b :: l₂) a)
⊢ a :: l₁ ~ b :: l₂
[PROOFSTEP]
exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm
