rw [Set.mem_mul]
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
x : α
⊢ x ∈ ↑t → x ∈ ↑t * ↑s
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
x : α
⊢ x ∈ ↑t → ∃ x_1 ∈ ↑t, ∃ y ∈ ↑s, x_1 * y = x