case h
G : Type ?u.238328
G' : Type ?u.238331
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.238340
inst✝² : AddGroup A
H K✝ : Subgroup G
k : Set G
N : Type u_1
inst✝¹ : Group N
P : Type ?u.238367
inst✝ : Group P
K : Subgroup N
x✝ : N
⊢ x✝ ∈ comap (MonoidHom.id N) K ↔ x✝ ∈ K
G : Type ?u.238328
G' : Type ?u.238331
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.238340
inst✝² : AddGroup A
H K✝ : Subgroup G
k : Set G
N : Type u_1
inst✝¹ : Group N
P : Type ?u.238367
inst✝ : Group P
K : Subgroup N
⊢ comap (MonoidHom.id N) K = K
ext
no goals
case h
G : Type ?u.238328
G' : Type ?u.238331
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.238340
inst✝² : AddGroup A
H K✝ : Subgroup G
k : Set G
N : Type u_1
inst✝¹ : Group N
P : Type ?u.238367
inst✝ : Group P
K : Subgroup N
x✝ : N
⊢ x✝ ∈ comap (MonoidHom.id N) K ↔ x✝ ∈ K
rfl