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

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
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ prod L ↔ ∃ a, a ∈ L ∧ p ∣ a
constructor
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
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
intro h
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

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
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
induction' L with L_hd L_tl L_ih
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
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
rw [prod_nil] at h
no goals
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
exact absurd h pp.not_dvd_one
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
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
rw [prod_cons] at h
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

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
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
cases' pp.dvd_or_dvd h with hd hd
no goals
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
exact ⟨L_hd, mem_cons_self L_hd L_tl, hd⟩
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
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
obtain ⟨x, hx1, hx2⟩ := L_ih hd
no goals
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
exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩
no goals
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
exact fun ⟨a, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod ha1)