rw [← image_coe_mul, ← coe_mul, preimage_image_quotientMk_mulStabilizer, coe_mul, image_coe_mul]
  at this
case inr.inr
ι : 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 * QuotientGroup.mk '' ↑t)) ≃
    ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card