no goals
G : Type u_2
G' : Type ?u.475486
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.475495
inst✝³ : AddGroup A
N✝ : Type ?u.475501
P : Type ?u.475504
inst✝² : Group N✝
inst✝¹ : Group P
K : Subgroup G
N : Type u_1
inst✝ : Group N
f : G →* N
⊢ ↑(range f) = ↑⊤ ↔ Set.range ↑f = Set.univ
rw [coe_range, coe_top]