rw [← Nat.card_prod, Nat.card_congr]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' t) = Nat.card ↑(t * ↑s)
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↥s × ↑(QuotientGroup.mk '' t) ≃ ↑(t * ↑s)