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 S
x : R × S
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (RingHom.snd R S) s
simp [mem_prod, MonoidHom.coe_snd]