no goals
G : Type u_1
G' : Type ?u.12139
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.12148
inst✝⁴ : AddGroup A
M : Type ?u.12154
S : Type u_2
inst✝³ : DivInvMonoid M
inst✝² : SetLike S M
hSM : SubgroupClass S M
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
x y : G
h : x ∈ H
this : SubmonoidClass S G
hba : y * x ∈ H
⊢ y ∈ H
simpa using mul_mem hba (inv_mem h)