simp_rw [← smul_eq_mul, ← biUnion_smul_finset, biUnion_congr rfl fun _ ↦ smul_mulStab,
  ← sup_eq_biUnion, sup_const hs.mulStab]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ s.mulStab * s.mulStab = s.mulStab
no goals