no goals
L : Language
M : Type w
N : Type u_1
P : Type ?u.972917
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
⊢ range f = ⊤ ↔ Function.Surjective ↑f
rw [SetLike.ext'_iff, range_coe, coe_top, Set.range_iff_surjective]