no goals
M : Type u_2
N✝ : Type ?u.61232
P : Type ?u.61235
σ : Type ?u.61238
inst✝³ : Mul M
inst✝² : Mul N✝
inst✝¹ : Mul P
S : Subsemigroup M
N : Type u_1
inst✝ : Mul N
f : M →ₙ* N
⊢ ↑(srange f) = ↑⊤ ↔ Set.range ↑f = Set.univ
rw [coe_srange, coe_top]