awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
n : ℕ
s : Fin n → M
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
⊢ ∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N

Tactic:
⟨range s, finite_range s, hs⟩

Premises used: Set.finite_range, And.intro, Exists.intro, Set.range
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
n : ℕ
s : Fin n → M
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
⊢ ∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N

Tactic:
exact ⟨range s, finite_range s, hs⟩
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
rw : Eq.{u_1 + 1} (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅) ⊥
rw₁ rw₂ : Eq.{u_1 + 1} (α := L.Substructure M) ⊥ ⊥
⊢ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑∅ : Set M)) ⊥

Tactic:
rw [Finset.coe_empty, closure_empty]

Premises used: Finset.coe_empty, FirstOrder.Language.Substructure.closure_empty
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
s : Set M
hs : s.Finite
rw rw₁ :
  Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)
⊢ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑(hs.toFinset (s := s)) : Set M))
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)

Tactic:
rw [hs.coe_toFinset]

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
x : M
⊢ FG (M := M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) {x})

Tactic:
fg_closure (finite_singleton x)

Premises used: FirstOrder.Language.Substructure.fg_closure, Set.finite_singleton
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₂ = N₂
rw :
  LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₁ ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₂ = N₁ ⊔ N₂
rw₁ : N₁ ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₂ = N₁ ⊔ N₂
rw₂ rw₃ : N₁ ⊔ N₂ = N₁ ⊔ N₂
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) (t₁ ∪ t₂) = N₁ ⊔ N₂

Tactic:
rw [closure_union, ht₁.2, ht₂.2]

Premises used: And.right, FirstOrder.Language.Substructure.closure_union
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M →[L] N
s : L.Substructure M
hs : s.FG
t : Set M
ht : t.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = s
rw : Substructure.map f (LowerAdjoint.toFun (u := SetLike.coe) (closure L) t) = Substructure.map f s
rw₁ rw₂ : Substructure.map f s = Substructure.map f s
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) '' t) = Substructure.map f s

Tactic:
rw [closure_image, ht.2]

Premises used: And.right, FirstOrder.Language.Substructure.closure_image
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
hs : (Substructure.map f.toHom s).FG
rcases :
  ∀ (t : Finset N) (h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s),
    s.FG
⊢ s.FG

Tactic:
rcases hs with ⟨t, h⟩
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s
rw : ∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = s
⊢ s.FG

Tactic:
rw [fg_def]

Premises used: FirstOrder.Language.Substructure.fg_def
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s
⊢ ∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = s

Tactic:
⟨f ⁻¹' t, t.finite_toSet.preimage f.injective.injOn, ?_⟩

Premises used: Function.Injective.injOn, SetLike.coe, Set.preimage, And.intro, Exists.intro, FirstOrder.Language.Embedding.injective, Finset.finite_toSet, DFunLike.coe, Set.Finite.preimage
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s
refine : LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' (↑t : Set N)) = s
⊢ ∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = s

Tactic:
refine ⟨f ⁻¹' t, t.finite_toSet.preimage f.injective.injOn, ?_⟩
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)

Tactic:
have hf : Function.Injective f.toHom := f.injective
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' (↑t : Set N)) = s

Tactic:
map_injective_of_injective hf ?_

Premises used: FirstOrder.Language.Substructure.map_injective_of_injective
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
refine :
  Substructure.map f.toHom (LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' (↑t : Set N))) =
    Substructure.map f.toHom s
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' (↑t : Set N)) = s

Tactic:
refine map_injective_of_injective hf ?_

Premises used: FirstOrder.Language.Substructure.map_injective_of_injective
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
rw : (↑t : Set N) ⊆ range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)
⊢ Substructure.map f.toHom (LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' (↑t : Set N))) =
    Substructure.map f.toHom s

Tactic:
rw [← h, map_closure, Embedding.coe_toHom, image_preimage_eq_of_subset]

Premises used: Set.image_preimage_eq_of_subset, FirstOrder.Language.Embedding.coe_toHom, FirstOrder.Language.Substructure.map_closure
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
x : N
hx : x ∈ (↑t : Set N)
⊢ x ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N)) : Set N)

Tactic:
have h' := subset_closure (L := L) hx
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
x : N
hx : x ∈ (↑t : Set N)
h' : x ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N)) : Set N)
⊢ x ∈ (↑(Substructure.map f.toHom s) : Set N)

Tactic:
rw [h] at h'
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
x : N
hx : x ∈ (↑t : Set N)
h' : x ∈ (↑(Substructure.map f.toHom s) : Set N)
⊢ Membership.mem (γ := Set N) (range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) x

Tactic:
Hom.map_le_range h'

Premises used: Set.Mem, setOf, FirstOrder.Language.Hom.map_le_range, Set.range
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
x : N
hx : x ∈ (↑t : Set N)
h' : x ∈ (↑(Substructure.map f.toHom s) : Set N)
⊢ Membership.mem (γ := Set N) (range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) x

Tactic:
exact Hom.map_le_range h'

Premises used: FirstOrder.Language.Hom.map_le_range
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
s : L.Substructure M
h : Finite.{u_1 + 1} ↥s
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑(Finite.toFinset (s := (↑s : Set M)) h) : Set M) = s

Tactic:
simp only [Finite.coe_toFinset, closure_eq]

Premises used: Set.Finite.coe_toFinset, FirstOrder.Language.Substructure.closure_eq
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : L.IsRelational
S : L.Substructure M
h : S.FG
obtain : ∀ (s : Finset M), Finite.{u_1 + 1} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M))
⊢ Finite.{u_1 + 1} ↥S

Tactic:
obtain ⟨s, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : L.IsRelational
s : Finset M
⊢ (↑s : Set M).Finite

Tactic:
have hs := s.finite_toSet
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : L.IsRelational
s : Finset M
hs : (↑s : Set M).Finite
⊢ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)) : Set M).Finite

Tactic:
rw [← closure_eq_of_isRelational L (s : Set M)] at hs

Premises used: FirstOrder.Language.Substructure.closure_eq_of_isRelational, SetLike.coe
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : L.IsRelational
s : Finset M
hs : (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)) : Set M).Finite
⊢ Finite.{u_1 + 1} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M))

Tactic:
hs

Premises used: Set.Finite
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : L.IsRelational
s : Finset M
hs : (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)) : Set M).Finite
⊢ Finite.{u_1 + 1} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M))

Tactic:
exact hs
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : L.IsRelational
S : L.Substructure M
⊢ S.FG ↔ Finite.{u_1 + 1} ↥S

Tactic:
⟨FG.finite, fun _ => FG.of_finite⟩

Premises used: FirstOrder.Language.Substructure.FG.finite, Iff.intro, FirstOrder.Language.Substructure.FG.of_finite
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
⊢ N.CG ↔ ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N

Tactic:
Iff.refl _

Premises used: Iff.refl, FirstOrder.Language.Substructure.CG
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
h : N.FG
obtain :
  ∀ (s : Set M) (hf : s.Finite) (h : FG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)),
    CG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)
⊢ N.CG

Tactic:
obtain ⟨s, hf, rfl⟩ := fg_def.1 h

Premises used: FirstOrder.Language.Substructure.fg_def, Iff.mp, rfl
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
s : Set M
hf : s.Finite
h : FG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)
⊢ CG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)

Tactic:
⟨s, hf.countable, rfl⟩

Premises used: And.intro, FirstOrder.Language.Substructure.CG, Exists.intro, Set.Finite.countable, rfl
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
s : Set M
hf : s.Finite
h : FG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)
⊢ CG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)

Tactic:
exact ⟨s, hf.countable, rfl⟩
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
mp :
  (∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N) →
    (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
mpr :
  ((↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N) →
    ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
⊢ (∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N) ↔
    (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N

Tactic:
constructor
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
mp :
  ∀ (h : (↑N : Set M) = ∅),
    (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
mp₁ :
  ∀ (h : (↑N : Set M).Nonempty),
    (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
⊢ (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N

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

Premises used: Set.eq_empty_or_nonempty, SetLike.coe
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
h : (↑N : Set M) = ∅
⊢ (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N

Tactic:
Or.intro_left _ h

Premises used: Or.intro_left
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
h : (↑N : Set M) = ∅
⊢ (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N

Tactic:
exact Or.intro_left _ h

Premises used: Or.intro_left
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
h : (↑N : Set M).Nonempty
mp :
  ∀ (f : ℕ → M) (h' : S ∪ {h.some (s := (↑N : Set M))} = range f),
    (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
⊢ (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N

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

Premises used: Set.singleton_nonempty, Set.Nonempty.inr, Set.Countable.union, Set.countable_singleton, Set.Countable.exists_eq_range, Set.Nonempty.some
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
h : (↑N : Set M).Nonempty
f : ℕ → M
h' : S ∪ {h.some (s := (↑N : Set M))} = range f
⊢ (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N

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

Premises used: Or.intro_right, Exists.intro
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
h : (↑N : Set M).Nonempty
f : ℕ → M
h' : S ∪ {h.some (s := (↑N : Set M))} = range f
mp : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range f) = N
⊢ (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N

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

Premises used: Or.intro_right
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
h : (↑N : Set M).Nonempty
f : ℕ → M
h' : S ∪ {h.some (s := (↑N : Set M))} = range f
mp : {h.some (s := (↑N : Set M))} ⊆ (↑N : Set M)
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range f) = N

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

Premises used: sup_eq_left, FirstOrder.Language.Substructure.closure_union, FirstOrder.Language.Substructure.closure_le
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
h : (↑N : Set M).Nonempty
f : ℕ → M
h' : S ∪ {h.some (s := (↑N : Set M))} = range f
⊢ {h.some (s := (↑N : Set M))} ⊆ (↑N : Set M)

Tactic:
singleton_subset_iff.2 h.some_mem

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Nonempty.some_mem
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
h : (↑N : Set M).Nonempty
f : ℕ → M
h' : S ∪ {h.some (s := (↑N : Set M))} = range f
⊢ {h.some (s := (↑N : Set M))} ⊆ (↑N : Set M)

Tactic:
exact singleton_subset_iff.2 h.some_mem

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Nonempty.some_mem
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
h : (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
mpr : ∀ (h : (↑N : Set M) = ∅), ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
mpr₁ :
  ∀ (h : ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N),
    ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
⊢ ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N

Tactic:
rcases h with h | h
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
h : (↑N : Set M) = ∅
⊢ ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N

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

Premises used: FirstOrder.Language.Substructure.closure_eq_of_le, And.intro, Set.empty_subset, Exists.intro, EmptyCollection.emptyCollection, Set.countable_empty
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
h : (↑N : Set M) = ∅
mpr : N ≤ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅
⊢ ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N

Tactic:
refine ⟨∅, countable_empty, closure_eq_of_le (empty_subset _) ?_⟩
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
h : (↑N : Set M) = ∅
mpr : ∅ ⊆ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅) : Set M)
⊢ N ≤ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅

Tactic:
rw [← SetLike.coe_subset_coe, h]

Premises used: SetLike.coe_subset_coe
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
h : (↑N : Set M) = ∅
⊢ ∅ ⊆ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅) : Set M)

Tactic:
empty_subset _

Premises used: Set.empty_subset
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
h : (↑N : Set M) = ∅
⊢ ∅ ⊆ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅) : Set M)

Tactic:
exact empty_subset _

Premises used: Set.empty_subset
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
h : ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
mpr :
  ∀ (f : ℕ → M),
    ∃ (S : Set M),
      S.Countable ∧
        Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S)
          (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range f))
⊢ ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N

Tactic:
obtain ⟨f, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
f : ℕ → M
⊢ ∃ (S : Set M),
    S.Countable ∧
      Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S)
        (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range f))

Tactic:
⟨range f, countable_range _, rfl⟩

Premises used: Set.countable_range, And.intro, Exists.intro, Set.range, rfl
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
f : ℕ → M
⊢ ∃ (S : Set M),
    S.Countable ∧
      Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S)
        (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range f))

Tactic:
exact ⟨range f, countable_range _, rfl⟩
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
⊢ CG.{u_1, u_2, u_3} (L := L) (M := M) ⊥

Tactic:
fg_bot.cg

Premises used: FirstOrder.Language.Substructure.FG.cg, FirstOrder.Language.Substructure.fg_bot
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
s : Set M
hs : s.Countable
⊢ CG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)

Tactic:
⟨s, hs, rfl⟩

Premises used: And.intro, FirstOrder.Language.Substructure.CG, Exists.intro, rfl
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
x : M
⊢ CG (M := M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) {x})

Tactic:
(fg_closure_singleton x).cg

Premises used: FirstOrder.Language.Substructure.fg_closure_singleton, FirstOrder.Language.Substructure.FG.cg