G : Type ?u.4395
G' : Type ?u.4398
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.4407
inst✝² : AddGroup A
M : Type u_1
S : Type u_2
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H K : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x * y⁻¹ ∈ H
G : Type ?u.4395
G' : Type ?u.4398
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.4407
inst✝² : AddGroup A
M : Type u_1
S : Type u_2
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H K : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x / y ∈ H
rw [div_eq_mul_inv]
no goals
G : Type ?u.4395
G' : Type ?u.4398
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.4407
inst✝² : AddGroup A
M : Type u_1
S : Type u_2
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H K : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x * y⁻¹ ∈ H
exact mul_mem hx (inv_mem hy)