no goals
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
s : Subgroup α
g z : α
⊢ z ∈ {x | ↑x = ↑g} ↔ z ∈ g *l ↑s
rw [mem_leftCoset_iff, Set.mem_setOf_eq, eq_comm, QuotientGroup.eq, SetLike.mem_coe]