simp only [Set.mem_iUnion, Set.mem_preimage, Subtype.exists, exists_prop, forall_exists_index,
and_imp]
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
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ ∀ x_1 ∈ s, x * x_1 ∈ t → x ∈ t * ↑s