no goals
M : Type ?u.7514
N : Type ?u.7517
P : Type u_1
σ : Type ?u.7523
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
S : Subsemigroup P
⊢ ∀ (x : P), x ∈ comap (MulHom.id P) S ↔ x ∈ S
simp