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