case h
L : Language
M : Type w
N : Type u_1
P : Type ?u.835752
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
x✝ : N
⊢ x✝ ∈ range f ↔ x✝ ∈ Substructure.map f ⊤
L : Language
M : Type w
N : Type u_1
P : Type ?u.835752
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
⊢ range f = Substructure.map f ⊤
ext
no goals
case h
L : Language
M : Type w
N : Type u_1
P : Type ?u.835752
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
x✝ : N
⊢ x✝ ∈ range f ↔ x✝ ∈ Substructure.map f ⊤
simp