G : Type u_1
G' : Type ?u.602966
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.602975
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : ker f ≤ H
hK : ker f ≤ K
hf : comap f (map f H) = comap f (map f K)
⊢ H = K
G : Type u_1
G' : Type ?u.602966
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.602975
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : ker f ≤ H
hK : ker f ≤ K
hf : map f H = map f K
⊢ H = K
apply_fun comap f  at hf
no goals
G : Type u_1
G' : Type ?u.602966
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.602975
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : ker f ≤ H
hK : ker f ≤ K
hf : comap f (map f H) = comap f (map f K)
⊢ H = K
rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf