[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = N) → FG N
[PROOFSTEP]
rintro ⟨t', h, rfl⟩
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
t' : Set M
h : Set.Finite t'
⊢ FG (LowerAdjoint.toFun (closure L) t')
[PROOFSTEP]
rcases Finite.exists_finset_coe h with ⟨t, rfl⟩
[GOAL]
case intro.intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
t : Finset M
h : Set.Finite ↑t
⊢ FG (LowerAdjoint.toFun (closure L) ↑t)
[PROOFSTEP]
exact ⟨t, rfl⟩
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ FG N ↔ ∃ n s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
rw [fg_def]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = N) ↔ ∃ n s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
constructor
[GOAL]
case mp
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = N) → ∃ n s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
rintro ⟨S, Sfin, hS⟩
[GOAL]
case mp.intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Sfin : Set.Finite S
hS : LowerAdjoint.toFun (closure L) S = N
⊢ ∃ n s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding
[GOAL]
case mp.intro.intro.intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
n : ℕ
f : Fin n ↪ M
Sfin : Set.Finite (range ↑f)
hS : LowerAdjoint.toFun (closure L) (range ↑f) = N
⊢ ∃ n s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
exact ⟨n, f, hS⟩
[GOAL]
case mpr
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (∃ n s, LowerAdjoint.toFun (closure L) (range s) = N) → ∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = N
[PROOFSTEP]
rintro ⟨n, s, hs⟩
[GOAL]
case mpr.intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
n : ℕ
s : Fin n → M
hs : LowerAdjoint.toFun (closure L) (range s) = N
⊢ ∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = N
[PROOFSTEP]
refine' ⟨range s, finite_range s, hs⟩
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
⊢ LowerAdjoint.toFun (closure L) ↑∅ = ⊥
[PROOFSTEP]
rw [Finset.coe_empty, closure_empty]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
s : Set M
hs : Set.Finite s
⊢ LowerAdjoint.toFun (closure L) ↑(Finite.toFinset hs) = LowerAdjoint.toFun (closure L) s
[PROOFSTEP]
rw [hs.coe_toFinset]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N₁ N₂ : Substructure L M
hN₁ : FG N₁
hN₂ : FG N₂
t₁ : Set M
ht₁ : Set.Finite t₁ ∧ LowerAdjoint.toFun (closure L) t₁ = N₁
t₂ : Set M
ht₂ : Set.Finite t₂ ∧ LowerAdjoint.toFun (closure L) t₂ = N₂
⊢ LowerAdjoint.toFun (closure L) (t₁ ∪ t₂) = N₁ ⊔ N₂
[PROOFSTEP]
rw [closure_union, ht₁.2, ht₂.2]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M →[L] N
s : Substructure L M
hs : FG s
t : Set M
ht : Set.Finite t ∧ LowerAdjoint.toFun (closure L) t = s
⊢ LowerAdjoint.toFun (closure L) (↑f '' t) = Substructure.map f s
[PROOFSTEP]
rw [closure_image, ht.2]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
hs : FG (Substructure.map (Embedding.toHom f) s)
⊢ FG s
[PROOFSTEP]
rcases hs with ⟨t, h⟩
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
rw [fg_def]
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
refine' ⟨f ⁻¹' t, t.finite_toSet.preimage (f.injective.injOn _), _⟩
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
have hf : Function.Injective f.toHom := f.injective
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
refine' map_injective_of_injective hf _
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
rw [← h, map_closure, Embedding.coe_toHom, image_preimage_eq_of_subset]
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
intro x hx
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
have h' := subset_closure (L := L) hx
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
rw [h] at h' 
[GOAL]
case intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
exact Hom.map_le_range h'
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
h : FG N
⊢ CG N
[PROOFSTEP]
obtain ⟨s, hf, rfl⟩ := fg_def.1 h
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
s : Set M
hf : Set.Finite s
h : FG (LowerAdjoint.toFun (closure L) s)
⊢ CG (LowerAdjoint.toFun (closure L) s)
[PROOFSTEP]
refine' ⟨s, hf.countable, rfl⟩
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ CG N ↔ ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
rw [cg_def]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N) ↔
    ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
constructor
[GOAL]
case mp
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N) →
    ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
rintro ⟨S, Scount, hS⟩
[GOAL]
case mp.intro.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Scount : Set.Countable S
hS : LowerAdjoint.toFun (closure L) S = N
⊢ ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
cases' eq_empty_or_nonempty (N : Set M) with h h
[GOAL]
case mp.intro.intro.inl
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Scount : Set.Countable S
hS : LowerAdjoint.toFun (closure L) S = N
h : ↑N = ∅
⊢ ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
exact Or.intro_left _ h
[GOAL]
case mp.intro.intro.inr
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Scount : Set.Countable S
hS : LowerAdjoint.toFun (closure L) S = N
h : Set.Nonempty ↑N
⊢ ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
obtain ⟨f, h'⟩ := (Scount.union (Set.countable_singleton h.some)).exists_eq_range (singleton_nonempty h.some).inr
[GOAL]
case mp.intro.intro.inr.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Scount : Set.Countable S
hS : LowerAdjoint.toFun (closure L) S = N
h : Set.Nonempty ↑N
f : ℕ → M
h' : S ∪ {Set.Nonempty.some h} = range f
⊢ ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
[PROOFSTEP]
refine' Or.intro_right _ ⟨f, _⟩
[GOAL]
case mp.intro.intro.inr.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Scount : Set.Countable S
hS : LowerAdjoint.toFun (closure L) S = N
h : Set.Nonempty ↑N
f : ℕ → M
h' : S ∪ {Set.Nonempty.some h} = range f
⊢ LowerAdjoint.toFun (closure L) (range f) = N
[PROOFSTEP]
rw [← h', closure_union, hS, sup_eq_left, closure_le]
[GOAL]
case mp.intro.intro.inr.intro
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
S : Set M
Scount : Set.Countable S
hS : LowerAdjoint.toFun (closure L) S = N
h : Set.Nonempty ↑N
f : ℕ → M
h' : S ∪ {Set.Nonempty.some h} = range f
⊢ {Set.Nonempty.some h} ⊆ ↑N
[PROOFSTEP]
exact singleton_subset_iff.2 h.some_mem
[GOAL]
case mpr
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
⊢ (↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N) →
    ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N
[PROOFSTEP]
intro h
[GOAL]
case mpr
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅ ∨ ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N
[PROOFSTEP]
cases' h with h h
[GOAL]
case mpr.inl
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N
[PROOFSTEP]
refine' ⟨∅, countable_empty, closure_eq_of_le (empty_subset _) _⟩
[GOAL]
case mpr.inl
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅
⊢ N ≤ LowerAdjoint.toFun (closure L) ∅
[PROOFSTEP]
rw [← SetLike.coe_subset_coe, h]
[GOAL]
case mpr.inl
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅
⊢ ∅ ⊆ ↑(LowerAdjoint.toFun (closure L) ∅)
[PROOFSTEP]
exact empty_subset _
[GOAL]
case mpr.inr
L : Language
M : Type u_1
inst✝ : Structure L M
N : Substructure L M
h : ∃ s, LowerAdjoint.toFun (closure L) (range s) = N
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N
[PROOFSTEP]
obtain ⟨f, rfl⟩ := h
[GOAL]
case mpr.inr.intro
L : Language
M : Type u_1
inst✝ : Structure L M
f : ℕ → M
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = LowerAdjoint.toFun (closure L) (range f)
[PROOFSTEP]
exact ⟨range f, countable_range _, rfl⟩
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
N₁ N₂ : Substructure L M
hN₁ : CG N₁
hN₂ : CG N₂
t₁ : Set M
ht₁ : Set.Countable t₁ ∧ LowerAdjoint.toFun (closure L) t₁ = N₁
t₂ : Set M
ht₂ : Set.Countable t₂ ∧ LowerAdjoint.toFun (closure L) t₂ = N₂
⊢ LowerAdjoint.toFun (closure L) (t₁ ∪ t₂) = N₁ ⊔ N₂
[PROOFSTEP]
rw [closure_union, ht₁.2, ht₂.2]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M →[L] N
s : Substructure L M
hs : CG s
t : Set M
ht : Set.Countable t ∧ LowerAdjoint.toFun (closure L) t = s
⊢ LowerAdjoint.toFun (closure L) (↑f '' t) = Substructure.map f s
[PROOFSTEP]
rw [closure_image, ht.2]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
f : M ↪[L] N
s : Substructure L M
hs : CG (Substructure.map (Embedding.toHom f) s)
⊢ CG s
[PROOFSTEP]
rcases hs with ⟨t, h1, h2⟩
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
rw [cg_def]
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
refine' ⟨f ⁻¹' t, h1.preimage f.injective, _⟩
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
have hf : Function.Injective f.toHom := f.injective
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
refine' map_injective_of_injective hf _
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
rw [← h2, map_closure, Embedding.coe_toHom, image_preimage_eq_of_subset]
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
intro x hx
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
have h' := subset_closure (L := L) hx
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
rw [h2] at h' 
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
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
[PROOFSTEP]
exact Hom.map_le_range h'
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
s : Substructure L M
⊢ CG s ↔ Countable { x // x ∈ s }
[PROOFSTEP]
refine' ⟨_, fun h => ⟨s, h.to_set, s.closure_eq⟩⟩
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
s : Substructure L M
⊢ CG s → Countable { x // x ∈ s }
[PROOFSTEP]
rintro ⟨s, h, rfl⟩
[GOAL]
case intro.intro
L : Language
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
s : Set M
h : Set.Countable s
⊢ Countable { x // x ∈ LowerAdjoint.toFun (closure L) s }
[PROOFSTEP]
exact h.substructure_closure L
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
⊢ FG L M ↔ ∃ S, Set.Finite S ∧ LowerAdjoint.toFun (closure L) S = ⊤
[PROOFSTEP]
rw [fg_def, Substructure.fg_def]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : FG L M
f : M →[L] N
⊢ Substructure.FG (Hom.range f)
[PROOFSTEP]
rw [Hom.range_eq_map]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : FG L M
f : M →[L] N
⊢ Substructure.FG (map f ⊤)
[PROOFSTEP]
exact (fg_def.1 h).map f
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : FG L M
f : M →[L] N
hs : Function.Surjective ↑f
⊢ FG L N
[PROOFSTEP]
rw [← Hom.range_eq_top] at hs 
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : FG L M
f : M →[L] N
hs : Hom.range f = ⊤
⊢ FG L N
[PROOFSTEP]
rw [fg_def, ← hs]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : FG L M
f : M →[L] N
hs : Hom.range f = ⊤
⊢ Substructure.FG (Hom.range f)
[PROOFSTEP]
exact h.range f
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
⊢ CG L M ↔ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = ⊤
[PROOFSTEP]
rw [cg_def, Substructure.cg_def]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : CG L M
f : M →[L] N
⊢ Substructure.CG (Hom.range f)
[PROOFSTEP]
rw [Hom.range_eq_map]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : CG L M
f : M →[L] N
⊢ Substructure.CG (map f ⊤)
[PROOFSTEP]
exact (cg_def.1 h).map f
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : CG L M
f : M →[L] N
hs : Function.Surjective ↑f
⊢ CG L N
[PROOFSTEP]
rw [← Hom.range_eq_top] at hs 
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : CG L M
f : M →[L] N
hs : Hom.range f = ⊤
⊢ CG L N
[PROOFSTEP]
rw [cg_def, ← hs]
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
N : Type u_2
inst✝ : Structure L N
h : CG L M
f : M →[L] N
hs : Hom.range f = ⊤
⊢ Substructure.CG (Hom.range f)
[PROOFSTEP]
exact h.range f
[GOAL]
L : Language
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
⊢ CG L M ↔ Countable M
[PROOFSTEP]
rw [cg_def, Substructure.cg_iff_countable, topEquiv.toEquiv.countable_iff]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
⊢ FG S ↔ Structure.FG L { x // x ∈ S }
[PROOFSTEP]
rw [Structure.fg_def]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
⊢ FG S ↔ FG ⊤
[PROOFSTEP]
refine' ⟨fun h => FG.of_map_embedding S.subtype _, fun h => _⟩
[GOAL]
case refine'_1
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h : FG S
⊢ FG (map (Embedding.toHom (subtype S)) ⊤)
[PROOFSTEP]
rw [← Hom.range_eq_map, range_subtype]
[GOAL]
case refine'_1
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h : FG S
⊢ FG S
[PROOFSTEP]
exact h
[GOAL]
case refine'_2
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h : FG ⊤
⊢ FG S
[PROOFSTEP]
have h := h.map S.subtype.toHom
[GOAL]
case refine'_2
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h✝ : FG ⊤
h : FG (map (Embedding.toHom (subtype S)) ⊤)
⊢ FG S
[PROOFSTEP]
rw [← Hom.range_eq_map, range_subtype] at h 
[GOAL]
case refine'_2
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h✝ : FG ⊤
h : FG S
⊢ FG S
[PROOFSTEP]
exact h
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
⊢ CG S ↔ Structure.CG L { x // x ∈ S }
[PROOFSTEP]
rw [Structure.cg_def]
[GOAL]
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
⊢ CG S ↔ CG ⊤
[PROOFSTEP]
refine' ⟨fun h => CG.of_map_embedding S.subtype _, fun h => _⟩
[GOAL]
case refine'_1
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h : CG S
⊢ CG (map (Embedding.toHom (subtype S)) ⊤)
[PROOFSTEP]
rw [← Hom.range_eq_map, range_subtype]
[GOAL]
case refine'_1
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h : CG S
⊢ CG S
[PROOFSTEP]
exact h
[GOAL]
case refine'_2
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h : CG ⊤
⊢ CG S
[PROOFSTEP]
have h := h.map S.subtype.toHom
[GOAL]
case refine'_2
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h✝ : CG ⊤
h : CG (map (Embedding.toHom (subtype S)) ⊤)
⊢ CG S
[PROOFSTEP]
rw [← Hom.range_eq_map, range_subtype] at h 
[GOAL]
case refine'_2
L : Language
M : Type u_1
inst✝ : Structure L M
S : Substructure L M
h✝ : CG ⊤
h : CG S
⊢ CG S
[PROOFSTEP]
exact h
