case h.a
G : Type u_1
G' : Type u_2
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.690834
inst✝¹ : AddGroup A
N : Type ?u.690840
inst✝ : Group N
H : Subgroup G
e : G ≃* G'
x✝ : { x // x ∈ H }
⊢ ↑(↑(equivMapOfInjective H ↑e (_ : Injective ↑e)) x✝) = ↑(↑(MulEquiv.subgroupMap e H) x✝)
G : Type u_1
G' : Type u_2
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.690834
inst✝¹ : AddGroup A
N : Type ?u.690840
inst✝ : Group N
H : Subgroup G
e : G ≃* G'
⊢ equivMapOfInjective H ↑e (_ : Injective ↑e) = MulEquiv.subgroupMap e H
ext
no goals
case h.a
G : Type u_1
G' : Type u_2
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.690834
inst✝¹ : AddGroup A
N : Type ?u.690840
inst✝ : Group N
H : Subgroup G
e : G ≃* G'
x✝ : { x // x ∈ H }
⊢ ↑(↑(equivMapOfInjective H ↑e (_ : Injective ↑e)) x✝) = ↑(↑(MulEquiv.subgroupMap e H) x✝)
rfl