case mp
G : Type u_2
G' : Type ?u.263490
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.263499
inst✝² : AddGroup A
H✝ : Subgroup G
k : Set G
N : Type u_1
inst✝¹ : Group N
P : Type ?u.263526
inst✝ : Group P
H : Subgroup N
e : G ≃* N
⊢ map (↑e) (map (↑(MulEquiv.symm e)) H) = H

case mpr
G : Type u_2
G' : Type ?u.263490
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.263499
inst✝² : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_1
inst✝¹ : Group N
P : Type ?u.263526
inst✝ : Group P
e : G ≃* N
⊢ map (↑(MulEquiv.symm e)) (map (↑e) K) = K
G : Type u_2
G' : Type ?u.263490
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.263499
inst✝² : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type u_1
inst✝¹ : Group N
P : Type ?u.263526
inst✝ : Group P
H : Subgroup N
e : G ≃* N
⊢ map (↑(MulEquiv.symm e)) H = K ↔ map (↑e) K = H
constructor <;> rintro rfl
no goals
case mp
G : Type u_2
G' : Type ?u.263490
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.263499
inst✝² : AddGroup A
H✝ : Subgroup G
k : Set G
N : Type u_1
inst✝¹ : Group N
P : Type ?u.263526
inst✝ : Group P
H : Subgroup N
e : G ≃* N
⊢ map (↑e) (map (↑(MulEquiv.symm e)) H) = H
rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
  MulEquiv.coe_monoidHom_refl, map_id]
no goals
case mpr
G : Type u_2
G' : Type ?u.263490
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.263499
inst✝² : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_1
inst✝¹ : Group N
P : Type ?u.263526
inst✝ : Group P
e : G ≃* N
⊢ map (↑(MulEquiv.symm e)) (map (↑e) K) = K
rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
  MulEquiv.coe_monoidHom_refl, map_id]