no goals
ι : Type u_2
M : ι → Type u_1
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.597231
inst✝ : Monoid N
i : ι
x : M i
hne_one : x ≠ 1
⊢ prod (singleton x hne_one) = ↑of x
simp [toWord, prod, Word.prod]