∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : Semiring k] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) [inst_3 : IsLeftCancelMul G] (r : k) (x : G),
  (∀ (y : k), r * x • y = 0 ↔ y = 0) →
    (SkewMonoidAlgebra.single x r * f).support = Finset.map (mulLeftEmbedding x) f.support