rw [SetLike.mem_coe] at h₁mem h₂mem ⊢
G : Type u_1
inst✝ : Group G
H : Subgroup G
h₁ h₂ : G
h₁mem : h₁ ∈ ↑H
h₂mem : h₂ ∈ ↑H
⊢ h₁ * h₂⁻¹ ∈ ↑H
G : Type u_1
inst✝ : Group G
H : Subgroup G
h₁ h₂ : G
h₁mem : h₁ ∈ H
h₂mem : h₂ ∈ H
⊢ h₁ * h₂⁻¹ ∈ H