-- Mathlib/Data/List/Prime.lean
theorem Prime.dvd_prod_iff {p : M} {L : List M} (pp : Prime p) : p ∣ L.prod ↔ ∃ a ∈ L, p ∣ a

Proof state:
case mp.cons.inr.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a ∈ L_tl, p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
x : M
hx1 : x ∈ L_tl
hx2 : p ∣ x
⊢ ∃ a ∈ L_hd :: L_tl, p ∣ a

Tactic:
exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩

Result:
no goals

Proof state:
case mp.cons.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a ∈ L_tl, p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
⊢ ∃ a ∈ L_hd :: L_tl, p ∣ a

Tactic:
obtain ⟨x, hx1, hx2⟩ := L_ih hd

Result:
case mp.cons.inr.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a ∈ L_tl, p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
x : M
hx1 : x ∈ L_tl
hx2 : p ∣ x
⊢ ∃ a ∈ L_hd :: L_tl, p ∣ a

Proof state:
case mp.nil
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
h : p ∣ 1
⊢ ∃ a ∈ [], p ∣ a

Tactic:
exact absurd h pp.not_dvd_one

Result:
no goals

Proof state:
case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ (∃ a ∈ L, p ∣ a) → p ∣ L.prod

Tactic:
exact fun ⟨a, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod ha1)

Result:
no goals

Proof state:
case mp.cons
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a ∈ L_tl, p ∣ a
h : p ∣ L_hd * L_tl.prod
⊢ ∃ a ∈ L_hd :: L_tl, p ∣ a

Tactic:
rcases pp.dvd_or_dvd h with hd | hd

Result:
case mp.cons.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a ∈ L_tl, p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_hd
⊢ ∃ a ∈ L_hd :: L_tl, p ∣ a

case mp.cons.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a ∈ L_tl, p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
⊢ ∃ a ∈ L_hd :: L_tl, p ∣ a

Proof state:
case mp.cons
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a ∈ L_tl, p ∣ a
h : p ∣ (L_hd :: L_tl).prod
⊢ ∃ a ∈ L_hd :: L_tl, p ∣ a

Tactic:
rw [prod_cons] at h

Result:
case mp.cons
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a ∈ L_tl, p ∣ a
h : p ∣ L_hd * L_tl.prod
⊢ ∃ a ∈ L_hd :: L_tl, p ∣ a

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ L.prod ↔ ∃ a ∈ L, p ∣ a

Tactic:
constructor

Result:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ L.prod → ∃ a ∈ L, p ∣ a

case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ (∃ a ∈ L, p ∣ a) → p ∣ L.prod

Proof state:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h : p ∣ L.prod
⊢ ∃ a ∈ L, p ∣ a

Tactic:
induction' L with L_hd L_tl L_ih

Result:
case mp.nil
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
h : p ∣ [].prod
⊢ ∃ a ∈ [], p ∣ a

case mp.cons
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a ∈ L_tl, p ∣ a
h : p ∣ (L_hd :: L_tl).prod
⊢ ∃ a ∈ L_hd :: L_tl, p ∣ a

Proof state:
case mp.nil
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
h : p ∣ [].prod
⊢ ∃ a ∈ [], p ∣ a

Tactic:
rw [prod_nil] at h

Result:
case mp.nil
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
h : p ∣ 1
⊢ ∃ a ∈ [], p ∣ a

Proof state:
case mp.cons.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a ∈ L_tl, p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_hd
⊢ ∃ a ∈ L_hd :: L_tl, p ∣ a

Tactic:
exact ⟨L_hd, mem_cons_self L_hd L_tl, hd⟩

Result:
no goals

Proof state:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ L.prod → ∃ a ∈ L, p ∣ a

Tactic:
intro h

Result:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h : p ∣ L.prod
⊢ ∃ a ∈ L, p ∣ a