apply Equiv.trans (QuotientGroup.preimageMkEquivSubgroupProdSet _ _).symm
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↥s × ↑(QuotientGroup.mk '' t) ≃ ↑(t * ↑s)
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' t)) ≃ ↑(t * ↑s)