∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (i : ι) (g : G i) (w : Monoid.CoprodI.Word G)
  (h1 : w.fstIdx ≠ some i) (hg1 : g ≠ 1),
  (∀ (i_1 : ι) (g_1 : G i_1), ⟨i_1, g_1⟩ ∈ (Monoid.CoprodI.Word.cons g w h1 hg1).toList → g_1 ∈ d.set i_1) →
    ∀ (x : ι) (x_1 : G x), ⟨x, x_1⟩ ∈ w.toList → x_1 ∈ d.set x