ι : Type ?u.9678
α : Type ?u.9681
M : Type u_1
N : Type ?u.9687
P : Type ?u.9690
M₀ : Type ?u.9693
G : Type ?u.9696
R : Type ?u.9699
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ prod l
ι : Type ?u.9678
α : Type ?u.9681
M : Type u_1
N : Type ?u.9687
P : Type ?u.9690
M₀ : Type ?u.9693
G : Type ?u.9696
R : Type ?u.9699
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
⊢ a ∣ prod l
let ⟨s, t, h⟩ := mem_split ha
ι : Type ?u.9678
α : Type ?u.9681
M : Type u_1
N : Type ?u.9687
P : Type ?u.9690
M₀ : Type ?u.9693
G : Type ?u.9696
R : Type ?u.9699
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ a * (prod s * prod t)
ι : Type ?u.9678
α : Type ?u.9681
M : Type u_1
N : Type ?u.9687
P : Type ?u.9690
M₀ : Type ?u.9693
G : Type ?u.9696
R : Type ?u.9699
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ prod l
rw [h, prod_append, prod_cons, mul_left_comm]
no goals
ι : Type ?u.9678
α : Type ?u.9681
M : Type u_1
N : Type ?u.9687
P : Type ?u.9690
M₀ : Type ?u.9693
G : Type ?u.9696
R : Type ?u.9699
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ a * (prod s * prod t)
exact dvd_mul_right _ _