no goals
M : Type u_2
N : Type u_1
P : Type ?u.99119
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.99140
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Submonoid N
x : M × N
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (MonoidHom.snd M N) s
simp [mem_prod, MonoidHom.coe_snd]