case inl
ι : Type u_1
α : Type ?u.154080
M : Type u_2
N : Type ?u.154086
P : Type ?u.154089
M₀ : Type ?u.154092
G : Type ?u.154095
R : Type ?u.154098
inst✝¹ : DecidableEq ι
inst✝ : CommMonoid M
f : ι → M
a : ι
l : List ι
h : a ∈ a :: l
⊢ f a * prod (map f (List.erase (a :: l) a)) = prod (map f (a :: l))

case inr.intro
ι : Type u_1
α : Type ?u.154080
M : Type u_2
N : Type ?u.154086
P : Type ?u.154089
M₀ : Type ?u.154092
G : Type ?u.154095
R : Type ?u.154098
inst✝¹ : DecidableEq ι
inst✝ : CommMonoid M
f : ι → M
a b : ι
l : List ι
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * prod (map f (List.erase (b :: l) a)) = prod (map f (b :: l))
ι : Type u_1
α : Type ?u.154080
M : Type u_2
N : Type ?u.154086
P : Type ?u.154089
M₀ : Type ?u.154092
G : Type ?u.154095
R : Type ?u.154098
inst✝¹ : DecidableEq ι
inst✝ : CommMonoid M
f : ι → M
a b : ι
l : List ι
h : a ∈ b :: l
⊢ f a * prod (map f (List.erase (b :: l) a)) = prod (map f (b :: l))
obtain rfl | ⟨ne, h⟩ := Decidable.List.eq_or_ne_mem_of_mem h
no goals
case inl
ι : Type u_1
α : Type ?u.154080
M : Type u_2
N : Type ?u.154086
P : Type ?u.154089
M₀ : Type ?u.154092
G : Type ?u.154095
R : Type ?u.154098
inst✝¹ : DecidableEq ι
inst✝ : CommMonoid M
f : ι → M
a : ι
l : List ι
h : a ∈ a :: l
⊢ f a * prod (map f (List.erase (a :: l) a)) = prod (map f (a :: l))
simp only [map, erase_cons_head, prod_cons]
no goals
case inr.intro
ι : Type u_1
α : Type ?u.154080
M : Type u_2
N : Type ?u.154086
P : Type ?u.154089
M₀ : Type ?u.154092
G : Type ?u.154095
R : Type ?u.154098
inst✝¹ : DecidableEq ι
inst✝ : CommMonoid M
f : ι → M
a b : ι
l : List ι
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * prod (map f (List.erase (b :: l) a)) = prod (map f (b :: l))
simp only [map, erase_cons_tail _ ne.symm, prod_cons, prod_map_erase _ h,
  mul_left_comm (f a) (f b)]