have h1 : Fintype.card ((s * t : Finset α) : Set α) = Fintype.card (s * t) := by congr
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
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp : Fintype.card ↑↑(s * t) = (s * t).mulStab.card * Fintype.card ↑(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
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp : Fintype.card ↑↑(s * t) = (s * t).mulStab.card * Fintype.card ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
h1 : Fintype.card ↑↑(s * t) = Fintype.card { x // x ∈ s * t }
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card