∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Fintype β] {s : Finset α} {f : α → Equiv.Perm β}
  {comm : (↑s).Pairwise (Function.onFun Commute f)} {x : β},
  x ∈ (s.noncommProd f comm).support → ∃ a ∈ s, x ∈ (f a).support