simp only [hab, mulStab_empty, smul_finset_empty, empty_subset]
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hs₁ : (s ∩ a • C.mulStab).Nonempty
ht₁ : (t ∩ b • C.mulStab).Nonempty
hab : C = ∅
⊢ (a * b) • C.mulStab ⊆ s * t
no goals