no goals
G : Type u_1
G' : Type ?u.297763
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.297772
inst✝² : AddGroup A
H K✝ : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.297799
inst✝ : Group P
K : Subgroup G
x : G × N
⊢ x ∈ prod K ⊤ ↔ x ∈ comap (MonoidHom.fst G N) K
simp [mem_prod, MonoidHom.coe_fst]