-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem cg_iff_empty_or_exists_nat_generating_family {N : L.Substructure M} :
    N.CG ↔ N = (∅ : Set M) ∨ ∃ s : ℕ → M, closure L (range s) = N

Proof state:
case mpr.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N

Tactic:
refine ⟨∅, countable_empty, closure_eq_of_le (empty_subset _) ?_⟩

Result:
case mpr.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅
⊢ N ≤ (closure L).toFun ∅

Proof state:
case mp.intro.intro.inr.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ {h.some} ⊆ ↑N

Tactic:
exact singleton_subset_iff.2 h.some_mem

Result:
no goals

Proof state:
case mpr.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ∃ s, (closure L).toFun (range s) = N
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N

Tactic:
obtain ⟨f, rfl⟩ := h

Result:
case mpr.inr.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
f : ℕ → M
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = (closure L).toFun (range f)

Proof state:
case mp.intro.intro.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : ↑N = ∅
⊢ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Tactic:
exact Or.intro_left _ h

Result:
no goals

Proof state:
case mpr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N

Tactic:
rcases h with h | h

Result:
case mpr.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N

case mpr.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ∃ s, (closure L).toFun (range s) = N
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N

Proof state:
case mp.intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
⊢ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Tactic:
rcases eq_empty_or_nonempty (N : Set M) with h | h

Result:
case mp.intro.intro.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : ↑N = ∅
⊢ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

case mp.intro.intro.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
⊢ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Proof state:
case mp
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Countable ∧ (closure L).toFun S = N) → ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Tactic:
rintro ⟨S, Scount, hS⟩

Result:
case mp.intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
⊢ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Proof state:
case mpr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N) → ∃ S, S.Countable ∧ (closure L).toFun S = N

Tactic:
intro h

Result:
case mpr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = N

Proof state:
case mpr.inr.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
f : ℕ → M
⊢ ∃ S, S.Countable ∧ (closure L).toFun S = (closure L).toFun (range f)

Tactic:
exact ⟨range f, countable_range _, rfl⟩

Result:
no goals

Proof state:
case mpr.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅
⊢ ∅ ⊆ ↑((closure L).toFun ∅)

Tactic:
exact empty_subset _

Result:
no goals

Proof state:
case mp.intro.intro.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
⊢ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Tactic:
obtain ⟨f, h'⟩ :=
  (Scount.union (Set.countable_singleton h.some)).exists_eq_range
    (singleton_nonempty h.some).inr

Result:
case mp.intro.intro.inr.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Proof state:
case mp.intro.intro.inr.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ (closure L).toFun (range f) = N

Tactic:
rw [← h', closure_union, hS, sup_eq_left, closure_le]

Result:
case mp.intro.intro.inr.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ {h.some} ⊆ ↑N

Proof state:
case mp.intro.intro.inr.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Tactic:
refine Or.intro_right _ ⟨f, ?_⟩

Result:
case mp.intro.intro.inr.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ (closure L).toFun (range f) = N

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ N.CG ↔ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Tactic:
rw [cg_def]

Result:
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Countable ∧ (closure L).toFun S = N) ↔ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Proof state:
case mpr.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅
⊢ N ≤ (closure L).toFun ∅

Tactic:
rw [← SetLike.coe_subset_coe, h]

Result:
case mpr.inl
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : ↑N = ∅
⊢ ∅ ⊆ ↑((closure L).toFun ∅)

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Countable ∧ (closure L).toFun S = N) ↔ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Tactic:
constructor

Result:
case mp
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Countable ∧ (closure L).toFun S = N) → ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

case mpr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N) → ∃ S, S.Countable ∧ (closure L).toFun S = N