no goals
M : Type u_2
N : Type u_1
P : Type ?u.51321
σ : Type ?u.51324
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
s : Subsemigroup N
x : M × N
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (MulHom.snd M N) s
simp [mem_prod, MulHom.coe_snd]