constructor
case h.e'_5.h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ t * ↑s ↔ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t
case h.e'_5.h.mp
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ t * ↑s → x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t

case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t → x ∈ t * ↑s