∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] {H : ι → Type u_5} [inst_1 : (i : ι) → Group (H i)]
  (f : (i : ι) → H i →* G) {α : Type u_6} [inst_2 : MulAction G α] (X : ι → Set α),
  (∀ (i : ι), (X i).Nonempty) →
    Pairwise (Function.onFun Disjoint X) →
      (Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i) →
        ∀ [Nontrivial ι] {i : ι} (w : Monoid.CoprodI.NeWord H i i), (Monoid.CoprodI.lift f) w.prod ≠ 1