no goals
M : Type u_2
N : Type u_1
P : Type ?u.118478
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.118499
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type u_3
mc : MonoidHomClass F M N
f : F
⊢ ↑(mrange f) = ↑⊤ ↔ Set.range ↑f = Set.univ
rw [coe_mrange, coe_top]