no goals
ι : Type u_1
M : ι → Type ?u.643406
inst✝² : (i : ι) → Monoid (M i)
N : Type ?u.643417
inst✝¹ : Monoid N
G : ι → Type u_2
inst✝ : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
⊢ prod (inv w) = (prod w)⁻¹
induction w <;> simp [inv, *]