rw [mul_mulStab_mul_mul_mul_mulStab_mul]
case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * (s * t).mulStab * (t * (s * t).mulStab)).card + (s * (s * t).mulStab * (t * (s * t).mulStab)).mulStab.card =
    (s * t).card + (s * t).mulStab.card
no goals