no goals
G : Type u_1
H : Type ?u.1244
A : Type ?u.1247
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
hs : IsSubgroup s
x y : G
hx : x ∈ s
hy : y ∈ s
⊢ x / y ∈ s
simpa only [div_eq_mul_inv] using hs.mul_mem hx (hs.inv_mem hy)