no goals
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Subsemiring R
x : R × S
⊢ x ∈ prod s ⊤ ↔ x ∈ comap (RingHom.fst R S) s
simp [mem_prod, MonoidHom.coe_fst]