simpa [mul_comm, disjoint_comm, mulStab_mul]
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
this : Disjoint (a • s.mulStab) (s * s.mulStab)
⊢ Disjoint s (a • s.mulStab)
no goals