no goals
ι : Type u_2
M : ι → Type u_1
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
f g : FreeProduct M →* N
h : ∀ (i : ι), MonoidHom.comp f of = MonoidHom.comp g of
x✝ : (i : ι) × M i
i : ι
x : M i
⊢ ↑(MonoidHom.comp f (Con.mk' (conGen (Rel M)))) (FreeMonoid.of { fst := i, snd := x }) =
    ↑(MonoidHom.comp g (Con.mk' (conGen (Rel M)))) (FreeMonoid.of { fst := i, snd := x })
rw [MonoidHom.comp_apply, MonoidHom.comp_apply, ← of_apply, ← MonoidHom.comp_apply, ←
  MonoidHom.comp_apply, h]