case h
L : Language
M : Type w
N : Type ?u.1144938
P : Type ?u.1144941
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
x : M
⊢ x ∈ Hom.range (Embedding.toHom (subtype S)) ↔ x ∈ S
L : Language
M : Type w
N : Type ?u.1144938
P : Type ?u.1144941
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
⊢ Hom.range (Embedding.toHom (subtype S)) = S
ext x
case h
L : Language
M : Type w
N : Type ?u.1144938
P : Type ?u.1144941
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
x : M
⊢ (∃ y, ↑y = x) ↔ x ∈ S
case h
L : Language
M : Type w
N : Type ?u.1144938
P : Type ?u.1144941
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
x : M
⊢ x ∈ Hom.range (Embedding.toHom (subtype S)) ↔ x ∈ S
simp only [Hom.mem_range, Embedding.coe_toHom, coeSubtype]
case h
L : Language
M : Type w
N : Type ?u.1144938
P : Type ?u.1144941
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
x : M
⊢ (∃ y, ↑y = x) → x ∈ S
case h
L : Language
M : Type w
N : Type ?u.1144938
P : Type ?u.1144941
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
x : M
⊢ (∃ y, ↑y = x) ↔ x ∈ S
refine' ⟨_, fun h => ⟨⟨x, h⟩, rfl⟩⟩
case h.intro.mk
L : Language
M : Type w
N : Type ?u.1144938
P : Type ?u.1144941
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
y : M
hy : y ∈ S
⊢ ↑{ val := y, property := hy } ∈ S
case h
L : Language
M : Type w
N : Type ?u.1144938
P : Type ?u.1144941
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
x : M
⊢ (∃ y, ↑y = x) → x ∈ S
rintro ⟨⟨y, hy⟩, rfl⟩
no goals
case h.intro.mk
L : Language
M : Type w
N : Type ?u.1144938
P : Type ?u.1144941
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
y : M
hy : y ∈ S
⊢ ↑{ val := y, property := hy } ∈ S
exact hy