∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Monoid (G i)] [inst_1 : Monoid H]
  {φ : (i : ι) → H →* G i} (i : ι) (g : G i), Monoid.PushoutI.ofCoprodI (Monoid.CoprodI.of g) = (Monoid.PushoutI.of i) g