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

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.Countable S ∧ LowerAdjoint.toFun (closure L) S = N
L : Language
M : Type u_3
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
constructor
case mp.intro.intro
L : Language
M : Type u_3
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
case mp
L : Language
M : Type u_3
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
rintro ⟨S, Scount, hS⟩
case mp.intro.intro.inl
L : Language
M : Type u_3
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

case mp.intro.intro.inr
L : Language
M : Type u_3
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
case mp.intro.intro
L : Language
M : Type u_3
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
cases' eq_empty_or_nonempty (N : Set M) with h h
case mp.intro.intro.inr.intro
L : Language
M : Type u_3
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
case mp.intro.intro.inr
L : Language
M : Type u_3
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
obtain ⟨f, h'⟩ :=
  (Scount.union (Set.countable_singleton h.some)).exists_eq_range
    (singleton_nonempty h.some).inr
case mp.intro.intro.inr.intro
L : Language
M : Type u_3
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
case mp.intro.intro.inr.intro
L : Language
M : Type u_3
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
refine' Or.intro_right _ ⟨f, _⟩
case mp.intro.intro.inr.intro
L : Language
M : Type u_3
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
case mp.intro.intro.inr.intro
L : Language
M : Type u_3
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
rw [← h', closure_union, hS, sup_eq_left, closure_le]
no goals
case mp.intro.intro.inr.intro
L : Language
M : Type u_3
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
exact singleton_subset_iff.2 h.some_mem
no goals
case mp.intro.intro.inl
L : Language
M : Type u_3
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
exact Or.intro_left _ h
case mpr
L : Language
M : Type u_3
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
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.Countable S ∧ LowerAdjoint.toFun (closure L) S = N
intro h
case mpr.inl
L : Language
M : Type u_3
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N

case mpr.inr
L : Language
M : Type u_3
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
case mpr
L : Language
M : Type u_3
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
cases' h with h h
case mpr.inl
L : Language
M : Type u_3
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅
⊢ N ≤ LowerAdjoint.toFun (closure L) ∅
case mpr.inl
L : Language
M : Type u_3
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = N
refine' ⟨∅, countable_empty, closure_eq_of_le (empty_subset _) _⟩
case mpr.inl
L : Language
M : Type u_3
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅
⊢ ∅ ⊆ ↑(LowerAdjoint.toFun (closure L) ∅)
case mpr.inl
L : Language
M : Type u_3
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅
⊢ N ≤ LowerAdjoint.toFun (closure L) ∅
rw [← SetLike.coe_subset_coe, h]
no goals
case mpr.inl
L : Language
M : Type u_3
inst✝ : Structure L M
N : Substructure L M
h : ↑N = ∅
⊢ ∅ ⊆ ↑(LowerAdjoint.toFun (closure L) ∅)
exact empty_subset _
case mpr.inr.intro
L : Language
M : Type u_3
inst✝ : Structure L M
f : ℕ → M
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = LowerAdjoint.toFun (closure L) (range f)
case mpr.inr
L : Language
M : Type u_3
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
obtain ⟨f, rfl⟩ := h
no goals
case mpr.inr.intro
L : Language
M : Type u_3
inst✝ : Structure L M
f : ℕ → M
⊢ ∃ S, Set.Countable S ∧ LowerAdjoint.toFun (closure L) S = LowerAdjoint.toFun (closure L) (range f)
exact ⟨range f, countable_range _, rfl⟩