no goals
R : Type u
S : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.268477
inst✝ : NonUnitalRingHomClass F R S
s : NonUnitalSubsemiring S
x : R × S
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (NonUnitalRingHom.snd R S) s
simp [mem_prod, MonoidHom.coe_snd]