rw [← SetLike.coe_sort_coe, ← coe_mulStab (hs.mul ht), Finset.coe_sort_coe]
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑(s * t))) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑(s * t))
⊢ ↥(stabilizer α (s * t)) = { x // x ∈ (s * t).mulStab }
no goals