awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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: classical
  refine (congr_arg _ (Set.ext <| Quotient.forall.2 fun N => ?_)).mp
    (countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)
  constructor
  · rintro ⟨s, hs⟩
    use Bundled.of (closure L (s : Set M))
    exact ⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩
  · simp only [mem_range, Quotient.eq]
    rintro ⟨P, ⟨⟨s, hs⟩, ⟨PM⟩⟩, hP2⟩
    refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩
    rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]
    exact ⟨PM.equivRange.symm⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
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⟧
⊢ Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' L.age M)
have mp : ∀ (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: classical
  refine (congr_arg _ (Set.ext <| Quotient.forall.2 fun N => ?_)).mp
    (countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)
  constructor
  · rintro ⟨s, hs⟩
    use Bundled.of (closure L (s : Set M))
    exact ⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩
  · simp only [mem_range, Quotient.eq]
    rintro ⟨P, ⟨⟨s, hs⟩, ⟨PM⟩⟩, hP2⟩
    refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩
    rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]
    exact ⟨PM.equivRange.symm⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
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⟧
mp :
  ∀ (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⟧
⊢ Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' L.age M)
have mpr : ∀ (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⟧
Tactic: classical
  refine (congr_arg _ (Set.ext <| Quotient.forall.2 fun N => ?_)).mp
    (countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)
  constructor
  · rintro ⟨s, hs⟩
    use Bundled.of (closure L (s : Set M))
    exact ⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩
  · simp only [mem_range, Quotient.eq]
    rintro ⟨P, ⟨⟨s, hs⟩, ⟨PM⟩⟩, hP2⟩
    refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩
    rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]
    exact ⟨PM.equivRange.symm⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
⊢ L.age (DirectLimit G f) = ⋃ (i : ι), L.age (G i)
have h : ∀ (M : Bundled L.Structure),
  M ∈ L.age (DirectLimit G f) ↔ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ι), L.age (G i)) M
Tactic: ext M
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
⊢ M ∈ L.age (DirectLimit G f) ↔ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ι), L.age (G i)) M
have h : M ∈ L.age (DirectLimit G f) ↔ ∃ (i : ι), M ∈ L.age (G i)
Tactic: simp only [mem_iUnion]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
⊢ M ∈ L.age (DirectLimit G f) ↔ ∃ (i : ι), M ∈ L.age (G i)
have h : M ∈ L.age (DirectLimit G f) → ∃ (i : ι), M ∈ L.age (G i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
h : M ∈ L.age (DirectLimit G f) → ∃ (i : ι), M ∈ L.age (G i)
⊢ M ∈ L.age (DirectLimit G f) ↔ ∃ (i : ι), M ∈ L.age (G i)
have h₁ : (∃ (i : ι), M ∈ L.age (G i)) → M ∈ L.age (DirectLimit G f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
⊢ ∃ (i : ι), M ∈ L.age (G i)
have h : ∀ (s : Finset (DirectLimit G f))
  (hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range),
  ∃ (i : ι), M ∈ L.age (G i)
Tactic: obtain ⟨s, hs⟩ := Mfg.range e.toHom
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
⊢ ∃ (i : ι), M ∈ L.age (G i)
have h : ∀ (i : ι) (hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i), ∃ (i : ι), M ∈ L.age (G i)
Tactic: obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
⊢ ∃ (i : ι), M ∈ L.age (G i)
have h : ∀ (e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i), ∃ (i : ι), M ∈ L.age (G i)
Tactic: have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i
⊢ ∃ (i : ι), M ∈ L.age (G i)
have h : e.toHom.range ≤ Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))
Tactic: refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i
⊢ e.toHom.range ≤ Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))
have h : (↑s : Set (DirectLimit G f)) ⊆ (↑(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) : Set (DirectLimit G f))
Tactic: rw [← hs, closure_le]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i
x : DirectLimit G f
hx : x ∈ (↑s : Set (DirectLimit G f))
⊢ x ∈ (↑(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) : Set (DirectLimit G f))
have h : (Embedding.toHom (DirectLimit.of L ι G f i) : (a : G i) → DirectLimit G f)
    ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i sorry : (a : G (out x).fst) → G i)
      ((out x).snd (β := fun (i : ι) ↦ G i))) =
  x
Tactic: refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i
x : DirectLimit G f
hx : x ∈ (↑s : Set (DirectLimit G f))
⊢ (Embedding.toHom (DirectLimit.of L ι G f i) : (a : G i) → DirectLimit G f)
      ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
        ((out x).snd (β := fun (i : ι) ↦ G i))) =
    x
have h : (DirectLimit.of L ι G f i : (a : G i) → DirectLimit G f)
    ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i sorry : (a : G (out x).fst) → G i)
      ((out x).snd (β := fun (i : ι) ↦ G i))) =
  x
Tactic: rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
      DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
      DirectedSystem.map_self]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i
x : DirectLimit G f
hx : x ∈ (↑s : Set (DirectLimit G f))
h :
  (DirectLimit.of L ι G f i : (a : G i) → DirectLimit G f)
      ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
        ((out x).snd (β := fun (i : ι) ↦ G i))) =
    x
⊢ (Embedding.toHom (DirectLimit.of L ι G f i) : (a : G i) → DirectLimit G f)
      ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
        ((out x).snd (β := fun (i : ι) ↦ G i))) =
    x
have h₁ : ⟦Structure.Sigma.mk (G := G) f i
      ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i sorry : (a : G (out x).fst) → G i)
        ((out x).snd (β := fun (i : ι) ↦ G i)))⟧ =
  x
Tactic: rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
      DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
      DirectedSystem.map_self]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i
x : DirectLimit G f
hx : x ∈ (↑s : Set (DirectLimit G f))
h :
  (DirectLimit.of L ι G f i : (a : G i) → DirectLimit G f)
      ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
        ((out x).snd (β := fun (i : ι) ↦ G i))) =
    x
h₁ :
  ⟦Structure.Sigma.mk (G := G) f i
        ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
          ((out x).snd (β := fun (i : ι) ↦ G i)))⟧ =
    x
⊢ (Embedding.toHom (DirectLimit.of L ι G f i) : (a : G i) → DirectLimit G f)
      ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
        ((out x).snd (β := fun (i : ι) ↦ G i))) =
    x
have h₂ : Structure.Sigma.mk (G := G) f i
    ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i sorry : (a : G (out x).fst) → G i)
      ((out x).snd (β := fun (i : ι) ↦ G i))) ≈
  Quotient.out x
Tactic: rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
      DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
      DirectedSystem.map_self]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
⊢ L.age (DirectLimit G f) = ⋃ (i : ι), L.age (G i)
have h : ∀ (M : Bundled L.Structure),
  M ∈ L.age (DirectLimit G f) ↔ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ι), L.age (G i)) M
Tactic: classical
  ext M
  simp only [mem_iUnion]
  constructor
  · rintro ⟨Mfg, ⟨e⟩⟩
    obtain ⟨s, hs⟩ := Mfg.range e.toHom
    let out := @Quotient.out _ (DirectLimit.setoid G f)
    obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))
    have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
    refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩
    rw [← hs, closure_le]
    intro x hx
    refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩
    rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
      DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
      DirectedSystem.map_self]
  · rintro ⟨i, Mfg, ⟨e⟩⟩
    exact ⟨Mfg, ⟨Embedding.comp (DirectLimit.of L ι G f i) e⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
h :
  ∀ (M : Bundled L.Structure),
    M ∈ L.age (DirectLimit G f) ↔ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ι), L.age (G i)) M
⊢ L.age (DirectLimit G f) = ⋃ (i : ι), L.age (G i)
have h₁ : ∀ (M : Bundled L.Structure), M ∈ L.age (DirectLimit G f) ↔ ∃ (i : ι), M ∈ L.age (G i)
Tactic: classical
  ext M
  simp only [mem_iUnion]
  constructor
  · rintro ⟨Mfg, ⟨e⟩⟩
    obtain ⟨s, hs⟩ := Mfg.range e.toHom
    let out := @Quotient.out _ (DirectLimit.setoid G f)
    obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))
    have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
    refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩
    rw [← hs, closure_le]
    intro x hx
    refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩
    rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
      DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
      DirectedSystem.map_self]
  · rintro ⟨i, Mfg, ⟨e⟩⟩
    exact ⟨Mfg, ⟨Embedding.comp (DirectLimit.of L ι G f i) e⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
h :
  ∀ (M : Bundled L.Structure),
    M ∈ L.age (DirectLimit G f) ↔ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ι), L.age (G i)) M
h₁ : ∀ (M : Bundled L.Structure), M ∈ L.age (DirectLimit G f) ↔ ∃ (i : ι), M ∈ L.age (G i)
⊢ L.age (DirectLimit G f) = ⋃ (i : ι), L.age (G i)
have h₂ : ∀ M ∈ L.age (DirectLimit G f), ∃ (i : ι), M ∈ L.age (G i)
Tactic: classical
  ext M
  simp only [mem_iUnion]
  constructor
  · rintro ⟨Mfg, ⟨e⟩⟩
    obtain ⟨s, hs⟩ := Mfg.range e.toHom
    let out := @Quotient.out _ (DirectLimit.setoid G f)
    obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))
    have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
    refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩
    rw [← hs, closure_le]
    intro x hx
    refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩
    rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
      DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
      DirectedSystem.map_self]
  · rintro ⟨i, Mfg, ⟨e⟩⟩
    exact ⟨Mfg, ⟨Embedding.comp (DirectLimit.of L ι G f i) e⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
h :
  ∀ (M : Bundled L.Structure),
    M ∈ L.age (DirectLimit G f) ↔ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ι), L.age (G i)) M
h₁ : ∀ (M : Bundled L.Structure), M ∈ L.age (DirectLimit G f) ↔ ∃ (i : ι), M ∈ L.age (G i)
h₂ : ∀ M ∈ L.age (DirectLimit G f), ∃ (i : ι), M ∈ L.age (G i)
⊢ L.age (DirectLimit G f) = ⋃ (i : ι), L.age (G i)
have h₃ : ∀ (M : Bundled L.Structure), (∃ (i : ι), M ∈ L.age (G i)) → M ∈ L.age (DirectLimit G f)
Tactic: classical
  ext M
  simp only [mem_iUnion]
  constructor
  · rintro ⟨Mfg, ⟨e⟩⟩
    obtain ⟨s, hs⟩ := Mfg.range e.toHom
    let out := @Quotient.out _ (DirectLimit.setoid G f)
    obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))
    have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
    refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩
    rw [← hs, closure_le]
    intro x hx
    refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩
    rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
      DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
      DirectedSystem.map_self]
  · rintro ⟨i, Mfg, ⟨e⟩⟩
    exact ⟨Mfg, ⟨Embedding.comp (DirectLimit.of L ι G f i) e⟩⟩