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