case h
L : Language
M : Type w
N : Type u_1
P : Type ?u.1142600
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ≃[L] N
n : N
⊢ n ∈ Hom.range (toHom f) ↔ n ∈ ⊤
L : Language
M : Type w
N : Type u_1
P : Type ?u.1142600
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ≃[L] N
⊢ Hom.range (toHom f) = ⊤
ext n
case h
L : Language
M : Type w
N : Type u_1
P : Type ?u.1142600
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ≃[L] N
n : N
⊢ ∃ y, ↑f y = n
case h
L : Language
M : Type w
N : Type u_1
P : Type ?u.1142600
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ≃[L] N
n : N
⊢ n ∈ Hom.range (toHom f) ↔ n ∈ ⊤
simp only [Hom.mem_range, coe_toHom, Substructure.mem_top, iff_true_iff]
no goals
case h
L : Language
M : Type w
N : Type u_1
P : Type ?u.1142600
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ≃[L] N
n : N
⊢ ∃ y, ↑f y = n
exact ⟨f.symm n, apply_symm_apply _ _⟩