rw [MulMemClass.mk_mul_mk, Subgroup.coe_mk, Subgroup.coe_mk, Subgroup.coe_mk, mul_left_inj]
case mk.mk
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∈ H
b : G
hb : b ∈ H
⊢ ↑({ val := a, property := ha } * { val := b, property := hb }) =
    ↑{ val := a, property := ha } * ↑{ val := b, property := hb }
no goals