no goals
L : Language
M : Type w
N : Type u_1
P : Type ?u.984407
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
p : Substructure L N
⊢ range f ≤ p ↔ comap f p = ⊤
rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]