awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
⊢ ∼φ ⇔[T] ∼ψ
have simp_rw : ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
  ¬φ.Realize v xs ↔ ¬ψ.Realize v xs
Tactic: simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
    BoundedFormula.realize_not]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ φ' ψ' : L.BoundedFormula α n
h : φ ⇔[T] ψ
h' : φ' ⇔[T] ψ'
⊢ φ ⟹ φ' ⇔[T] ψ ⟹ ψ'
have simp_rw : ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
  φ.Realize v xs → φ'.Realize v xs ↔ ψ.Realize v xs → ψ'.Realize v xs
Tactic: simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
    BoundedFormula.realize_imp]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⇔ ∀' liftAt 1 n φ).Realize v xs
have rw : φ.Realize v xs ↔ (∀' liftAt 1 n φ).Realize v xs
Tactic: rw [realize_iff, realize_all_liftAt_one_self]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
rw : φ.Realize v xs ↔ (∀' liftAt 1 n φ).Realize v xs
⊢ (φ ⇔ ∀' liftAt 1 n φ).Realize v xs
have rw₁ : φ.Realize v xs ↔ φ.Realize v xs
Tactic: rw [realize_iff, realize_all_liftAt_one_self]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
t' : Set M
h : t'.Finite
⊢ FG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) t')
have rcases : ∀ (t : Finset M) (h : (↑t : Set M).Finite), FG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set M))
Tactic: rcases Finite.exists_finset_coe h with ⟨t, rfl⟩
Cleared hypotheses: t', h
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
⊢ N.FG ↔ ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
have rw : (∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N) ↔
  ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
Tactic: rw [fg_def]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
⊢ (∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N) ↔
    ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
have mp : (∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N) →
  ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
mp :
  (∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N) →
    ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
⊢ (∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N) ↔
    ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
have mpr : (∃ (n : ℕ) (s : Fin n → M), 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: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
S : Set M
Sfin : S.Finite
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
⊢ ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
have mp : ∀ (n : ℕ) (f : Fin n ↪ M) (Sfin : Set.Finite (α := M) (range (ι := Fin n) (⇑f : (a : Fin n) → M)))
  (hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range (ι := Fin n) (⇑f : (a : Fin n) → M)) = N),
  ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
Tactic: obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding
Cleared hypotheses: S, Sfin, hS
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
⊢ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑∅ : Set M)) ⊥
have rw : Eq.{u_1 + 1} (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅) ⊥
Tactic: rw [Finset.coe_empty, closure_empty]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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) ∅) ⊥
⊢ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑∅ : Set M)) ⊥
have rw₁ : Eq.{u_1 + 1} (α := L.Substructure M) ⊥ ⊥
Tactic: rw [Finset.coe_empty, closure_empty]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
s : Set M
hs : s.Finite
⊢ 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)
have rw : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)
  (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)
Tactic: rw [hs.coe_toFinset]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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₂
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) (t₁ ∪ t₂) = N₁ ⊔ N₂
have rw : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₁ ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₂ = N₁ ⊔ N₂
Tactic: rw [closure_union, ht₁.2, ht₂.2]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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₂
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) (t₁ ∪ t₂) = N₁ ⊔ N₂
have rw₁ : N₁ ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₂ = N₁ ⊔ N₂
Tactic: rw [closure_union, ht₁.2, ht₂.2]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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₂
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) (t₁ ∪ t₂) = N₁ ⊔ N₂
have rw₂ : N₁ ⊔ N₂ = N₁ ⊔ N₂
Tactic: rw [closure_union, ht₁.2, ht₂.2]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) '' t) = Substructure.map f s
have rw : Substructure.map f (LowerAdjoint.toFun (u := SetLike.coe) (closure L) t) = Substructure.map f s
Tactic: rw [closure_image, ht.2]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) '' t) = Substructure.map f s
have rw₁ : Substructure.map f s = Substructure.map f s
Tactic: rw [closure_image, ht.2]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
⊢ s.FG
have rcases : ∀ (t : Finset N) (h : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N) = Substructure.map f.toHom s), s.FG
Tactic: rcases hs with ⟨t, h⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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.FG
have rw : ∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = s
Tactic: rw [fg_def]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
have refine : LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' (↑t : Set N)) = s
Tactic: refine ⟨f ⁻¹' t, t.finite_toSet.preimage f.injective.injOn, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (hypothesis)
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
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' (↑t : Set N)) = s
have hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
Tactic: have hf : Function.Injective f.toHom := f.injective
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
have refine : Substructure.map f.toHom (LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' (↑t : Set N))) =
  Substructure.map f.toHom s
Tactic: refine map_injective_of_injective hf ?_
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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)
⊢ Substructure.map f.toHom (LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' (↑t : Set N))) =
    Substructure.map f.toHom s
have rw : (↑t : Set N) ⊆ range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)
Tactic: rw [← h, map_closure, Embedding.coe_toHom, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (hypothesis)
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)
⊢ Membership.mem (γ := Set N) (range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) x
have h' : x ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set N)) : Set N)
Tactic: have h' := subset_closure (L := L) hx
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (hypothesis)
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)
⊢ Membership.mem (γ := Set N) (range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) x
have h'₁ : x ∈ (↑(Substructure.map f.toHom s) : Set N)
Tactic: rw [h] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : L.IsRelational
S : L.Substructure M
h : S.FG
⊢ Finite.{u_1 + 1} ↥S
have obtain : ∀ (s : Finset M), Finite.{u_1 + 1} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M))
Tactic: obtain ⟨s, rfl⟩ := h
Cleared hypotheses: S, h
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : L.IsRelational
s : Finset M
⊢ Finite.{u_1 + 1} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M))
have hs : (↑s : Set M).Finite
Tactic: have hs := s.finite_toSet
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : L.IsRelational
s : Finset M
hs : (↑s : Set M).Finite
⊢ Finite.{u_1 + 1} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M))
have hs₁ : (↑(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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
h : N.FG
⊢ N.CG
have 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)
Tactic: obtain ⟨s, hf, rfl⟩ := fg_def.1 h
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
⊢ (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
have mp : ∀ (h : (↑N : Set M) = ∅),
  (↑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
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
⊢ (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
have mp₁ : ∀ (h : (↑N : Set M).Nonempty),
  (↑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
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
⊢ (↑N : Set M) = ∅ ∨ ∃ (s : ℕ → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
have 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
Tactic: obtain ⟨f, h'⟩ :=
      (Scount.union (Set.countable_singleton h.some)).exists_eq_range
        (singleton_nonempty h.some).inr
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
have mp : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range f) = N
Tactic: refine Or.intro_right _ ⟨f, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range f) = N
have mp : {h.some (s := (↑N : Set M))} ⊆ (↑N : Set M)
Tactic: rw [← h', closure_union, hS, sup_eq_left, closure_le]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
⊢ ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
have mpr : ∀ (h : (↑N : Set M) = ∅), ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
⊢ ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
have 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
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
have mpr : N ≤ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅
Tactic: refine ⟨∅, countable_empty, closure_eq_of_le (empty_subset _) ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
h : (↑N : Set M) = ∅
⊢ N ≤ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅
have mpr : ∅ ⊆ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅) : Set M)
Tactic: rw [← SetLike.coe_subset_coe, h]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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
⊢ ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
have 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))
Tactic: obtain ⟨f, rfl⟩ := h
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.CG
hN₂ : N₂.CG
t₁ : Set M
ht₁ : t₁.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₁ = N₁
t₂ : Set M
ht₂ : t₂.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₂ = N₂
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) (t₁ ∪ t₂) = N₁ ⊔ N₂
have rw : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₁ ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₂ = N₁ ⊔ N₂
Tactic: rw [closure_union, ht₁.2, ht₂.2]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.CG
hN₂ : N₂.CG
t₁ : Set M
ht₁ : t₁.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₁ = N₁
t₂ : Set M
ht₂ : t₂.Countable ∧ 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₂
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) (t₁ ∪ t₂) = N₁ ⊔ N₂
have rw₁ : N₁ ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₂ = N₁ ⊔ N₂
Tactic: rw [closure_union, ht₁.2, ht₂.2]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.CG
hN₂ : N₂.CG
t₁ : Set M
ht₁ : t₁.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₁ = N₁
t₂ : Set M
ht₂ : t₂.Countable ∧ 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₂
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) (t₁ ∪ t₂) = N₁ ⊔ N₂
have rw₂ : N₁ ⊔ N₂ = N₁ ⊔ N₂
Tactic: rw [closure_union, ht₁.2, ht₂.2]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
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.CG
t : Set M
ht : t.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = s
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) '' t) = Substructure.map f s
have rw : Substructure.map f (LowerAdjoint.toFun (u := SetLike.coe) (closure L) t) = Substructure.map f s
Tactic: rw [closure_image, ht.2]