case inl
ι : Type ?u.150239
α : Type ?u.150242
M : Type u_1
N : Type ?u.150248
P : Type ?u.150251
M₀ : Type ?u.150254
G : Type ?u.150257
R : Type ?u.150260
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
a : M
l : List M
h : a ∈ a :: l
⊢ a * prod (List.erase (a :: l) a) = prod (a :: l)

case inr.intro
ι : Type ?u.150239
α : Type ?u.150242
M : Type u_1
N : Type ?u.150248
P : Type ?u.150251
M₀ : Type ?u.150254
G : Type ?u.150257
R : Type ?u.150260
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
a b : M
l : List M
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ a * prod (List.erase (b :: l) a) = prod (b :: l)
ι : Type ?u.150239
α : Type ?u.150242
M : Type u_1
N : Type ?u.150248
P : Type ?u.150251
M₀ : Type ?u.150254
G : Type ?u.150257
R : Type ?u.150260
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
a b : M
l : List M
h : a ∈ b :: l
⊢ a * prod (List.erase (b :: l) a) = prod (b :: l)
obtain rfl | ⟨ne, h⟩ := Decidable.List.eq_or_ne_mem_of_mem h
no goals
case inl
ι : Type ?u.150239
α : Type ?u.150242
M : Type u_1
N : Type ?u.150248
P : Type ?u.150251
M₀ : Type ?u.150254
G : Type ?u.150257
R : Type ?u.150260
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
a : M
l : List M
h : a ∈ a :: l
⊢ a * prod (List.erase (a :: l) a) = prod (a :: l)
simp only [List.erase, if_pos, prod_cons, beq_self_eq_true]
no goals
case inr.intro
ι : Type ?u.150239
α : Type ?u.150242
M : Type u_1
N : Type ?u.150248
P : Type ?u.150251
M₀ : Type ?u.150254
G : Type ?u.150257
R : Type ?u.150260
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
a b : M
l : List M
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ a * prod (List.erase (b :: l) a) = prod (b :: l)
simp only [List.erase, beq_false_of_ne ne.symm, prod_cons, prod_erase h, mul_left_comm a b]