no goals
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N : Type ?u.392300
inst✝¹ : Monoid N
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head = 1
⊢ prod (rcons p) = ↑of p.head * prod p.tail
rw [rcons, dif_pos hm, hm, MonoidHom.map_one, one_mul]
no goals
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N : Type ?u.392300
inst✝¹ : Monoid N
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head = 1
⊢ prod (rcons p) = ↑of p.head * prod p.tail
rw [rcons, dif_neg hm, prod, List.map_cons, List.prod_cons, prod]