α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a *l ↑s = ↑s
⊢ a ∈ a *l ↑s
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a *l ↑s = ↑s
⊢ a ∈ s
rw [← SetLike.mem_coe, ← ha]
no goals
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a *l ↑s = ↑s
⊢ a ∈ a *l ↑s
exact mem_own_leftCoset s a