simp_rw [@not_imp_comm (_ ⊆ _), ← smul_eq_mul, ← biUnion_smul_finset, disjoint_biUnion_right,
  Classical.not_forall]
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ¬a • s.mulStab ⊆ t * s.mulStab → Disjoint (a • s.mulStab) (t * s.mulStab)
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (∃ x, ∃ (_ : x ∈ t), ¬Disjoint (a • s.mulStab) (x • s.mulStab)) → a • s.mulStab ⊆ t.biUnion fun x => x • s.mulStab