awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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).CG
⊢ s.CG
have rcases : ∀ (t : Set N) (h1 : t.Countable)
  (h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s), s.CG
Tactic: rcases hs with ⟨t, h1, h2⟩
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 : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s
⊢ ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = s
have refine : LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' t) = s
Tactic: refine ⟨f ⁻¹' t, h1.preimage f.injective, ?_⟩
-- 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 : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' t) = 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 : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = 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) = s
have refine : Substructure.map f.toHom (LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' t)) =
  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 : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = 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)) =
    Substructure.map f.toHom s
have rw : t ⊆ range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)
Tactic: rw [← h2, 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 : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = 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
⊢ 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)
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 : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = 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
h' : x ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) t) : 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 [h2] 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 : Countable.{u_2 + 1} ((l : ℕ) × L.Functions l)
s : L.Substructure M
⊢ s.CG ↔ Countable.{u_1 + 1} ↥s
have refine : s.CG → Countable.{u_1 + 1} ↥s
Tactic: refine ⟨?_, fun h => ⟨s, h.to_set, s.closure_eq⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
⊢ FG L M ↔ ∃ (S : Set M), S.Finite ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
have rw : Substructure.FG.{u_1, u_2, u_3} (L := L) (M := M) ⊤ ↔
  ∃ (S : Set M), S.Finite ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
Tactic: rw [fg_def, Substructure.fg_def]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
rw :
  Substructure.FG.{u_1, u_2, u_3} (L := L) (M := M) ⊤ ↔
    ∃ (S : Set M), S.Finite ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
⊢ FG L M ↔ ∃ (S : Set M), S.Finite ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
have rw₁ : (∃ (S : Set M), S.Finite ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤) ↔
  ∃ (S : Set M), S.Finite ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
Tactic: rw [fg_def, Substructure.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
h : FG L M
f : M →[L] N
⊢ f.range.FG
have rw : (map f ⊤).FG
Tactic: rw [Hom.range_eq_map]
-- 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
h : FG L M
f : M →[L] N
hs : Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ FG L N
have hs₁ : f.range = ⊤
Tactic: rw [← Hom.range_eq_top] 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 : Type u_2
inst_1 : L.Structure N
h : FG L M
f : M →[L] N
hs : f.range = ⊤
⊢ FG L N
have rw : f.range.FG
Tactic: rw [fg_def, ← 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
inst_2 : Countable N
h : FG L M
⊢ Countable (M →[L] N)
have let : ∀ (S : Set M) (finite_S : S.Finite)
  (closure_S : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤), Countable (M →[L] N)
Tactic: let ⟨S, finite_S, closure_S⟩ := fg_iff.1 h
-- 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
inst_2 : Countable N
h_1 : FG L M
S : Set M
finite_S : S.Finite
closure_S : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
g : (M →[L] N) → (↑S : Type u_1) → N := fun (f : M →[L] N) ↦ (⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ S)
f f' : M →[L] N
h : g f = g f'
⊢ f = f'
have apply : EqOn.{u_1, u_2} (β := N) (⇑f : (a : M) → N) (⇑f' : (a : M) → N) S
Tactic: apply Hom.eq_of_eqOn_dense closure_S
-- 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
inst_2 : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
g : (M →[L] N) → (↑S : Type u_1) → N := fun (f : M →[L] N) ↦ (⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ S)
⊢ Countable (M →[L] N)
have g_inj : Function.Injective g
Tactic: have g_inj : Function.Injective g := by
    intro f f' h
    apply Hom.eq_of_eqOn_dense closure_S
    intro x x_in_S
    exact congr_fun h ⟨x, x_in_S⟩
-- 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
inst_2 : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
g : (M →[L] N) → (↑S : Type u_1) → N := fun (f : M →[L] N) ↦ (⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ S)
g_inj : Function.Injective g
⊢ Countable (M →[L] N)
have this : Finite.{u_1 + 1} (↑S : Type u_1)
Tactic: have : Finite ↑S := (S.finite_coe_iff).2 finite_S
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
⊢ CG L M ↔
    ∃ (S : Set M), S.Countable ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
have rw : Substructure.CG.{u_1, u_2, u_3} (L := L) (M := M) ⊤ ↔
  ∃ (S : Set M), S.Countable ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
Tactic: rw [cg_def, Substructure.cg_def]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
rw :
  Substructure.CG.{u_1, u_2, u_3} (L := L) (M := M) ⊤ ↔
    ∃ (S : Set M), S.Countable ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
⊢ CG L M ↔
    ∃ (S : Set M), S.Countable ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
have rw₁ : (∃ (S : Set M), S.Countable ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤) ↔
  ∃ (S : Set M), S.Countable ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
Tactic: rw [cg_def, Substructure.cg_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
h : CG L M
f : M →[L] N
⊢ f.range.CG
have rw : (map f ⊤).CG
Tactic: rw [Hom.range_eq_map]
-- 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
h : CG L M
f : M →[L] N
hs : Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ CG L N
have hs₁ : f.range = ⊤
Tactic: rw [← Hom.range_eq_top] 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 : Type u_2
inst_1 : L.Structure N
h : CG L M
f : M →[L] N
hs : f.range = ⊤
⊢ CG L N
have rw : f.range.CG
Tactic: rw [cg_def, ← hs]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable.{u_2 + 1} ((l : ℕ) × L.Functions l)
⊢ CG L M ↔ Countable M
have rw : Substructure.CG.{u_1, u_2, u_3} (L := L) (M := M) ⊤ ↔ Countable M
Tactic: rw [cg_def, Substructure.cg_iff_countable, topEquiv.toEquiv.countable_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable.{u_2 + 1} ((l : ℕ) × L.Functions l)
rw : Substructure.CG.{u_1, u_2, u_3} (L := L) (M := M) ⊤ ↔ Countable M
⊢ CG L M ↔ Countable M
have rw₁ : Countable.{u_1 + 1} ↥⊤ ↔ Countable M
Tactic: rw [cg_def, Substructure.cg_iff_countable, topEquiv.toEquiv.countable_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable.{u_2 + 1} ((l : ℕ) × L.Functions l)
rw : Substructure.CG.{u_1, u_2, u_3} (L := L) (M := M) ⊤ ↔ Countable M
rw₁ : Countable.{u_1 + 1} ↥⊤ ↔ Countable M
⊢ CG L M ↔ Countable M
have rw₂ : Countable M ↔ Countable M
Tactic: rw [cg_def, Substructure.cg_iff_countable, topEquiv.toEquiv.countable_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
⊢ S.FG ↔ Structure.FG.{u_1, u_2, u_3} L ↥S
have rw : S.FG ↔ FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
Tactic: rw [Structure.fg_def]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
⊢ S.FG ↔ FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
have refine_1 : ∀ (h : S.FG), (map S.subtype.toHom ⊤).FG
Tactic: refine ⟨fun h => FG.of_map_embedding S.subtype ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
refine_1 : ∀ (h : S.FG), (map S.subtype.toHom ⊤).FG
⊢ S.FG ↔ FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
have refine_2 : ∀ (h : FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤), S.FG
Tactic: refine ⟨fun h => FG.of_map_embedding S.subtype ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h : FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
⊢ S.FG
have h₁ : (map S.subtype.toHom ⊤).FG
Tactic: have h := h.map S.subtype.toHom
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
⊢ S.CG ↔ Structure.CG.{u_1, u_2, u_3} L ↥S
have rw : S.CG ↔ CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
Tactic: rw [Structure.cg_def]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
⊢ S.CG ↔ CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
have refine_1 : ∀ (h : S.CG), (map S.subtype.toHom ⊤).CG
Tactic: refine ⟨fun h => CG.of_map_embedding S.subtype ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
refine_1 : ∀ (h : S.CG), (map S.subtype.toHom ⊤).CG
⊢ S.CG ↔ CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
have refine_2 : ∀ (h : CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤), S.CG
Tactic: refine ⟨fun h => CG.of_map_embedding S.subtype ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h : CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
⊢ S.CG
have h₁ : (map S.subtype.toHom ⊤).CG
Tactic: have h := h.map S.subtype.toHom
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable M
g : { S : L.Substructure M // S.FG } → Finset M :=
  fun (S : { S : L.Substructure M // S.FG }) ↦
    Exists.choose (p := fun (a : Finset M) ↦
      LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯
S S' : { S : L.Substructure M // S.FG }
h : g S = g S'
⊢ S = S'
have a : (↑S : L.Substructure M) = (↑S' : L.Substructure M)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable M
g : { S : L.Substructure M // S.FG } → Finset M :=
  fun (S : { S : L.Substructure M // S.FG }) ↦
    Exists.choose (p := fun (a : Finset M) ↦
      LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯
S S' : { S : L.Substructure M // S.FG }
h : g S = g S'
⊢ (↑S : L.Substructure M) = (↑S' : L.Substructure M)
have a : Eq (α := L.Substructure M)
  (LowerAdjoint.toFun (u := SetLike.coe) (closure L)
    (↑(Exists.choose (p := fun (a : Finset M) ↦
          LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) sorry) :
      Set M))
  (LowerAdjoint.toFun (u := SetLike.coe) (closure L)
    (↑(Exists.choose (p := fun (a : Finset M) ↦
          LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S' : L.Substructure M)) sorry) :
      Set M))
Tactic: rw [(Exists.choose_spec S.prop).symm, (Exists.choose_spec S'.prop).symm]
-- Lean 4 proof step from Mathlib.ModelTheory.FinitelyGenerated (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable M
g : { S : L.Substructure M // S.FG } → Finset M :=
  fun (S : { S : L.Substructure M // S.FG }) ↦
    Exists.choose (p := fun (a : Finset M) ↦
      LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯
⊢ Countable.{max 1 (u_1 + 1)} { S : L.Substructure M // S.FG }
have g_inj : Function.Injective g
Tactic: have g_inj : Function.Injective g := by
    intro S S' h
    apply Subtype.ext
    rw [(Exists.choose_spec S.prop).symm, (Exists.choose_spec S'.prop).symm]
    exact congr_arg (closure L ∘ SetLike.coe) h
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
C : Quotient (α := Bundled L.Structure) equivSetoid
N : Bundled L.Structure
N_eq : Quotient.mk' N = C
N_fg : Structure.FG.{w, u, v} L (↑N : Type w)
N_incl : (↑N : Type w) ↪[L] M
⊢ ∃ (V : { V : L.Substructure M // V.FG }), ⟦{ α := ↥(↑V : L.Substructure M), str := inferInstance }⟧ = C
have refine : N_incl.toHom.range.FG
Tactic: refine N_eq.symm ▸ ⟨⟨N_incl.toHom.range, ?_⟩, Quotient.sound ⟨N_incl.equivRange.symm⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
⊢ Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' L.age M)
have refine : ∀ (N : Bundled L.Structure),
  Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid))
      (range fun (s : Finset M) ↦
        ⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧)
      ⟦N⟧ ↔
    Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧
Tactic: refine (congr_arg _ (Set.ext <| Quotient.forall.2 fun N => ?_)).mp
    (countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid))
      (range fun (s : Finset M) ↦
        ⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧)
      ⟦N⟧ ↔
    Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧
have mp : Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid))
    (range fun (s : Finset M) ↦
      ⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧)
    ⟦N⟧ →
  Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N : Bundled L.Structure
mp :
  Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid))
      (range fun (s : Finset M) ↦
        ⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧)
      ⟦N⟧ →
    Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧
⊢ Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid))
      (range fun (s : Finset M) ↦
        ⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧)
      ⟦N⟧ ↔
    Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧
have mpr : Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧ →
  Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid))
    (range fun (s : Finset M) ↦
      ⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧)
    ⟦N⟧
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N : Bundled L.Structure
s : Finset M
hs :
  Eq (α := Quotient (α := Bundled L.Structure) equivSetoid)
    ((fun (s : Finset M) ↦
        (⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧ :
          Quotient (α := Bundled L.Structure) equivSetoid))
      s)
    ⟦N⟧
⊢ Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧
have h₁ : Bundled.of ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)) ∈ L.age M ∧
  Eq (α := Quotient (α := Bundled L.Structure) equivSetoid)
    (Quotient.mk' (Bundled.of ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)))) ⟦N⟧
Tactic: use Bundled.of (closure L (s : Set M))
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧ →
    Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid))
      (range fun (s : Finset M) ↦
        ⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧)
      ⟦N⟧
have mpr : Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧ →
  ∃ (y : Finset M),
    (equivSetoid : Bundled L.Structure → Bundled L.Structure → Prop)
      { α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑y : Set M)), str := inferInstance } N
Tactic: simp only [mem_range, Quotient.eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Eq (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' P) ⟦N⟧
s : Finset (↑P : Type w)
hs :
  Eq (α := L.Substructure (↑P : Type w)) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (↑P : Type w))) ⊤
PM : (↑P : Type w) ↪[L] M
⊢ ∃ (y : Finset M),
    (equivSetoid : Bundled L.Structure → Bundled L.Structure → Prop)
      { α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑y : Set M)), str := inferInstance } N
have mpr : { α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑(Finset.image (⇑PM : (a : (↑P : Type w)) → M) s) : Set M)),
    str := inferInstance } ≈
  P
Tactic: refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Eq (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' P) ⟦N⟧
s : Finset (↑P : Type w)
hs :
  Eq (α := L.Substructure (↑P : Type w)) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (↑P : Type w))) ⊤
PM : (↑P : Type w) ↪[L] M
⊢ {
      α :=
        ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L)
            (↑(Finset.image (⇑PM : (a : (↑P : Type w)) → M) s) : Set M)),
      str := inferInstance } ≈
    P
have mpr : { α := ↥PM.toHom.range, str := inferInstance } ≈ P
Tactic: rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]