case 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 : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
⊢ FG 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 : FG (Substructure.map (Embedding.toHom f) s)
⊢ FG s
rcases hs with ⟨t, h⟩
case 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 : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
⊢ ∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = s
case 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 : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
⊢ FG s
rw [fg_def]
case 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 : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
⊢ LowerAdjoint.toFun (closure L) (↑f ⁻¹' ↑t) = s
case 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 : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
⊢ ∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = s
refine' ⟨f ⁻¹' t, t.finite_toSet.preimage (f.injective.injOn _), _⟩
case 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 : Finset N
h : 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
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 : Finset N
h : 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
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 : Finset N
h : 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
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 : Finset N
h : 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
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 : Finset N
h : LowerAdjoint.toFun (closure L) ↑t = Substructure.map (Embedding.toHom f) s
hf : Function.Injective ↑(Embedding.toHom f)
⊢ ↑t ⊆ range ↑f
case 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 : Finset N
h : 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 [← h, map_closure, Embedding.coe_toHom, image_preimage_eq_of_subset]
case 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 : Finset N
h : 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
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 : Finset N
h : 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
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 : Finset N
h : 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
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 : Finset N
h : 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
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 : Finset N
h : 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
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 : Finset N
h : 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 [h] at h'
no goals
case 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 : Finset N
h : 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'