Theorem: l1_2_2_ba' (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∀ (a b : ↥H), ↑(a * b) = ↑a * ↑b) ∧ ↑1 = 1
Tactic:
refine' ⟨_, Subgroup.coe_one _⟩
State after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (a b : ↥H), ↑(a * b) = ↑a * ↑b

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

State before:
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 }
Tactic:
rw [MulMemClass.mk_mul_mk, Subgroup.coe_mk, Subgroup.coe_mk, Subgroup.coe_mk, mul_left_inj]
State after:
no goals