rw [← mul_inv_cancel_right x y]
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x y : α
hys : y ∈ s
hxy : x * y ∈ t
⊢ x ∈ t * ↑s
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x y : α
hys : y ∈ s
hxy : x * y ∈ t
⊢ x * y * y⁻¹ ∈ t * ↑s