case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
⊢ CG s
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
hs : CG (Substructure.map (Embedding.toHom f) s)
⊢ CG s
rcases hs with ⟨t, h1, h2⟩
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = s
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
⊢ CG s
rw [cg_def]
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
⊢ LowerAdjoint.toFun (closure L) (↑f ⁻¹' t) = s
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = s
refine' ⟨f ⁻¹' t, h1.preimage f.injective, _⟩
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ LowerAdjoint.toFun (closure L) (↑f ⁻¹' t) = s
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
⊢ LowerAdjoint.toFun (closure L) (↑f ⁻¹' t) = s
have hf : Function.Injective f.toHom := f.injective
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ Substructure.map (Embedding.toHom f) (LowerAdjoint.toFun (closure L) (↑f ⁻¹' t)) =
    Substructure.map (Embedding.toHom f) s
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ LowerAdjoint.toFun (closure L) (↑f ⁻¹' t) = s
refine' map_injective_of_injective hf _
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ t ⊆ range ↑f
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ Substructure.map (Embedding.toHom f) (LowerAdjoint.toFun (closure L) (↑f ⁻¹' t)) =
    Substructure.map (Embedding.toHom f) s
rw [← h2, map_closure, Embedding.coe_toHom, image_preimage_eq_of_subset]
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
x : N
hx : x ∈ t
⊢ x ∈ range ↑f
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ t ⊆ range ↑f
intro x hx
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
x : N
hx : x ∈ t
h' : x ∈ ↑(LowerAdjoint.toFun (closure L) t)
⊢ x ∈ range ↑f
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
x : N
hx : x ∈ t
⊢ x ∈ range ↑f
have h' := subset_closure (L := L) hx
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
x : N
hx : x ∈ t
h' : x ∈ ↑(Substructure.map (Embedding.toHom f) s)
⊢ x ∈ range ↑f
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
x : N
hx : x ∈ t
h' : x ∈ ↑(LowerAdjoint.toFun (closure L) t)
⊢ x ∈ range ↑f
rw [h2] at h'
no goals
case intro.intro
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
t : Set N
h1 : Set.Countable t
h2 : LowerAdjoint.toFun (closure L) t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
x : N
hx : x ∈ t
h' : x ∈ ↑(Substructure.map (Embedding.toHom f) s)
⊢ x ∈ range ↑f
exact Hom.map_le_range h'