case intro.intro
L : Language
M : Type u_3
inst✝ : Structure L M
s : Set M
hf : Set.Finite s
h : FG (LowerAdjoint.toFun (closure L) s)
⊢ CG (LowerAdjoint.toFun (closure L) s)
L : Language
M : Type u_3
inst✝ : Structure L M
N : Substructure L M
h : FG N
⊢ CG N
obtain ⟨s, hf, rfl⟩ := fg_def.1 h
no goals
case intro.intro
L : Language
M : Type u_3
inst✝ : Structure L M
s : Set M
hf : Set.Finite s
h : FG (LowerAdjoint.toFun (closure L) s)
⊢ CG (LowerAdjoint.toFun (closure L) s)
refine' ⟨s, hf.countable, rfl⟩