rw [← coe_inj, coe_mulStab (hs.image _), ← stabilizer_coe_finset, ← stabilizer_coe_finset,
  coe_image, coe_one, stabilizer_image_coe_quotient, Subgroup.coe_bot, Set.singleton_one]
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ (image QuotientGroup.mk s).mulStab = 1
no goals