apply Set.BijOn.equiv id
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↑(⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t) ≃ ↑(t * ↑s)
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ Set.BijOn id (⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t) (t * ↑s)