∀ {α : Type u_4} {β : Type u_5} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α} [inst_2 : Mul β]
  [SMulCommClass α β β] [IsScalarTower α β β] {x y : β}, a ≠ 0 → Commute (a • x) y = Commute x y