∀ {H : Type u_3} [inst : Group H] {ι : Type u_5} {G : ι → Type u_6} [inst_1 : (i : ι) → Group (G i)]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ},
  Function.Injective Monoid.PushoutI.NormalWord.prod