rintro ⟨a, ha⟩ ⟨b, hb⟩
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (a b : ↥H), ↑(a * b) = ↑a * ↑b
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 }