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_1
inst✝¹ : NonUnitalNonAssocSemiring T
inst✝ : NonUnitalRingHomClass F R S
s : NonUnitalSubsemiring R
f : F
⊢ ↑(srange f) = ↑⊤ ↔ Set.range ↑f = Set.univ
rw [coe_srange, coe_top]