G : Type u_2
G' : Type u_1
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.427007
inst✝¹ : AddGroup A
H K : Subgroup G
f : G' →* G
hf : Injective ↑f
inst✝ : IsCommutative H
a b : { x // x ∈ comap f H }
this :
  { val := ↑f ↑a, property := (_ : ↑a ∈ comap f H) } * { val := ↑f ↑b, property := (_ : ↑b ∈ comap f H) } =
    { val := ↑f ↑b, property := (_ : ↑b ∈ comap f H) } * { val := ↑f ↑a, property := (_ : ↑a ∈ comap f H) }
⊢ ↑(a * b) = ↑(b * a)
G : Type u_2
G' : Type u_1
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.427007
inst✝¹ : AddGroup A
H K : Subgroup G
f : G' →* G
hf : Injective ↑f
inst✝ : IsCommutative H
a b : { x // x ∈ comap f H }
⊢ ↑(a * b) = ↑(b * a)
have := mul_comm (⟨f a, a.2⟩ : H) (⟨f b, b.2⟩ : H)
no goals
G : Type u_2
G' : Type u_1
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.427007
inst✝¹ : AddGroup A
H K : Subgroup G
f : G' →* G
hf : Injective ↑f
inst✝ : IsCommutative H
a b : { x // x ∈ comap f H }
this :
  { val := ↑f ↑a, property := (_ : ↑a ∈ comap f H) } * { val := ↑f ↑b, property := (_ : ↑b ∈ comap f H) } =
    { val := ↑f ↑b, property := (_ : ↑b ∈ comap f H) } * { val := ↑f ↑a, property := (_ : ↑a ∈ comap f H) }
⊢ ↑(a * b) = ↑(b * a)
rwa [Subtype.ext_iff, coe_mul, coe_mul, coe_mk, coe_mk, ← map_mul, ← map_mul,
  hf.eq_iff] at this