L : Language
M : Type u_3
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
L : Language
M : Type u_3
inst✝ : Structure L M
N : Substructure L M
⊢ FG N ↔ ∃ n s, LowerAdjoint.toFun (closure L) (range s) = N
rw [fg_def]
case mp
L : Language
M : Type u_3
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

case mpr
L : Language
M : Type u_3
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
L : Language
M : Type u_3
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
constructor
case mp.intro.intro
L : Language
M : Type u_3
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
case mp
L : Language
M : Type u_3
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
rintro ⟨S, Sfin, hS⟩
case mp.intro.intro.intro.intro
L : Language
M : Type u_3
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
case mp.intro.intro
L : Language
M : Type u_3
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
obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding
no goals
case mp.intro.intro.intro.intro
L : Language
M : Type u_3
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
exact ⟨n, f, hS⟩
case mpr.intro.intro
L : Language
M : Type u_3
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
case mpr
L : Language
M : Type u_3
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
rintro ⟨n, s, hs⟩
no goals
case mpr.intro.intro
L : Language
M : Type u_3
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
refine' ⟨range s, finite_range s, hs⟩