∀ {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 : IsRightCancelMul G] (r : k) (x : G),
  (∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0) →
    (f * SkewMonoidAlgebra.single x r).support = Finset.map (mulRightEmbedding x) f.support