apply disjoint_smul_finset_mulStab_mul_mulStab
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ Disjoint (a • s.mulStab) (s * s.mulStab)
case a
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hst : s ⊆ t
has : ¬a • s.mulStab ⊆ t
⊢ ¬a • s.mulStab ⊆ s * s.mulStab