awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
α : Type u_1
inst_5 : Finite α
x : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
a : α
r : ((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i) ≤ i
this :
  (Structure.Sigma.mk (G := G) f i
          ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
            ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).fst
      (β := fun (i : ι) ↦ G i) ≤
    i
⊢ Quotient.out (x a) ≈
    Structure.Sigma.mk (G := G) f i
      ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
        ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))
have h : Eq (α := G i)
  ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i sorry : (a : G (Quotient.out (x a)).fst) → G i)
      ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)) :
    G i)
  ((f
          ((Structure.Sigma.mk (G := G) f i
                ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
                  ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).fst
            (β := fun (i : ι) ↦ G i))
          i this :
        (a :
            G
              (Structure.Sigma.mk f i
                  ((f (Quotient.out (x a)).fst i r : (a : G (Quotient.out (x a)).fst) → G i)
                    (Quotient.out (x a)).snd)).fst) →
          G i)
      ((Structure.Sigma.mk (G := G) f i
            ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
              ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).snd
        (β := fun (i : ι) ↦ G i)) :
    G i)
Tactic: rw [equiv_iff G f (i := i) (hi _) this]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
α : Type u_1
inst_5 : Finite α
x : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
a : α
r : ((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i) ≤ i
this :
  (Structure.Sigma.mk (G := G) f i
          ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
            ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).fst
      (β := fun (i : ι) ↦ G i) ≤
    i
h :
  Eq (α := G i)
    ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (Quotient.out (x a)).fst) → G i)
        ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f
            ((Structure.Sigma.mk (G := G) f i
                  ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
                    ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).fst
              (β := fun (i : ι) ↦ G i))
            i this :
          (a :
              G
                (Structure.Sigma.mk f i
                    ((f (Quotient.out (x a)).fst i r : (a : G (Quotient.out (x a)).fst) → G i)
                      (Quotient.out (x a)).snd)).fst) →
            G i)
        ((Structure.Sigma.mk (G := G) f i
              ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
                ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).snd
          (β := fun (i : ι) ↦ G i)) :
      G i)
⊢ Quotient.out (x a) ≈
    Structure.Sigma.mk (G := G) f i
      ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
        ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))
have rw : Membership.mem (γ := Set ι) (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))
  ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))
Tactic: rw [equiv_iff G f (i := i) (hi _) this]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (hypothesis)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
i : ι
x y : G i
h :
  Eq (α := DirectLimit G f) ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) x)
    ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) y)
⊢ x = y
have h₁ : (setoid G f : Σˣ f → Σˣ f → Prop) (Structure.Sigma.mk (G := G) f i x) (Structure.Sigma.mk (G := G) f i y)
Tactic: rw [Quotient.eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
i : ι
x y : G i
h : (setoid G f : Σˣ f → Σˣ f → Prop) (Structure.Sigma.mk (G := G) f i x) (Structure.Sigma.mk (G := G) f i y)
⊢ x = y
have obtain : ∀ (j : ι) (h1 w : i ≤ j)
  (h3 : Eq (α := G j) ((f i j h1 : (a : G i) → G j) x : G j) ((f i j w : (a : G i) → G j) y : G j)), x = y
Tactic: obtain ⟨j, h1, _, h3⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
i : ι
n : ℕ
F : L.Functions n
x : Fin n → G i
⊢ ⟦Structure.Sigma.mk (G := G) f i (funMap F x)⟧ = funMap F ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) ∘ x)
have rw : Eq (α := DirectLimit G f) (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (x a)⟧)
  (funMap F ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) ∘ x))
Tactic: rw [← funMap_quotient_mk'_sigma_mk']
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
i : ι
n : ℕ
R : L.Relations n
x : Fin n → G i
⊢ RelMap (M := DirectLimit G f) R ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) ∘ x) ↔ RelMap R x
have change : (RelMap (M := Quotient (setoid G f)) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (x a)⟧) ↔ RelMap R x
Tactic: change RelMap R (fun a => (⟦.mk f i (x a)⟧ : DirectLimit G f)) ↔ _
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ Eq (α := DirectLimit G f)
    ((of L ι G f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G f)
    ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)
have rw : (setoid G f : Σˣ f → Σˣ f → Prop) (Structure.Sigma.mk (G := G) f j ((f i j hij : (a : G i) → G j) x))
  (Structure.Sigma.mk (G := G) f i x)
Tactic: rw [of_apply, of_apply, Quotient.eq]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (setoid G f : Σˣ f → Σˣ f → Prop) (Structure.Sigma.mk (G := G) f j ((f i j hij : (a : G i) → G j) x))
    (Structure.Sigma.mk (G := G) f i x)
have refine : Eq (α := G j) ((f i j hij : (a : G i) → G j) x : G j)
  ((f j j sorry : (a : G j) → G j) ((f i j hij : (a : G i) → G j) x : G j) : G j)
Tactic: refine Setoid.symm ⟨j, hij, refl j, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
⊢ ∃ (i : ι) (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S
have let : ∀ (A : Finset (DirectLimit G f))
  (A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S),
  ∃ (i : ι) (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S
Tactic: let ⟨A, A_closure⟩ := S_fg
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
⊢ ∃ (i : ι) (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S
have let : ∀ (i : ι) (y : ↥A → G i)
  (eq_y :
    Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
      ⟦Structure.Sigma.mk (G := G) f i (y a)⟧),
  ∃ (i : ι) (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S
Tactic: let ⟨i, y, eq_y⟩ := exists_quotient_mk'_sigma_mk'_eq G _ (fun a : A ↦ a.1)
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
⊢ ∃ (i : ι) (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S
have h : ∃ (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S
Tactic: use i
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
⊢ ∃ (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S
have h : Substructure.map (Embedding.toHom (of L ι G f i))
    (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (range y)) =
  S
Tactic: use Substructure.closure L (range y)
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
⊢ Substructure.map (Embedding.toHom (of L ι G f i))
      (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (range y)) =
    S
have h : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
    ((⇑(Embedding.toHom (of L ι G f i)) : (a : G i) → DirectLimit G f) '' range y) =
  S
Tactic: rw [Substructure.map_closure]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
⊢ LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' range y) =
    S
have h : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
    ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' y '' univ) =
  S
Tactic: rw [← image_univ, image_image, image_univ, ← eq_y,
    Subtype.range_coe_subtype, Finset.setOf_mem, A_closure]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
h :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' y '' univ) =
    S
⊢ LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' range y) =
    S
have h₁ : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
    ((fun (x : ↥A) ↦ ⟦Structure.Sigma.mk (G := G) f i (y x)⟧) '' univ) =
  S
Tactic: rw [← image_univ, image_image, image_univ, ← eq_y,
    Subtype.range_coe_subtype, Finset.setOf_mem, A_closure]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
h :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' y '' univ) =
    S
h₁ :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (x : ↥A) ↦ ⟦Structure.Sigma.mk (G := G) f i (y x)⟧) '' univ) =
    S
⊢ LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' range y) =
    S
have h₂ : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
    (range fun (x : ↥A) ↦ ⟦Structure.Sigma.mk (G := G) f i (y x)⟧) =
  S
Tactic: rw [← image_univ, image_image, image_univ, ← eq_y,
    Subtype.range_coe_subtype, Finset.setOf_mem, A_closure]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
h :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' y '' univ) =
    S
h₁ :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (x : ↥A) ↦ ⟦Structure.Sigma.mk (G := G) f i (y x)⟧) '' univ) =
    S
h₂ :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      (range fun (x : ↥A) ↦ ⟦Structure.Sigma.mk (G := G) f i (y x)⟧) =
    S
⊢ LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' range y) =
    S
have h₃ : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (range fun (a : ↥A) ↦ (↑a : DirectLimit G f)) = S
Tactic: rw [← image_univ, image_image, image_univ, ← eq_y,
    Subtype.range_coe_subtype, Finset.setOf_mem, A_closure]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
h :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' y '' univ) =
    S
h₁ :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (x : ↥A) ↦ ⟦Structure.Sigma.mk (G := G) f i (y x)⟧) '' univ) =
    S
h₂ :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      (range fun (x : ↥A) ↦ ⟦Structure.Sigma.mk (G := G) f i (y x)⟧) =
    S
h₃ : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (range fun (a : ↥A) ↦ (↑a : DirectLimit G f)) = S
⊢ LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' range y) =
    S
have h₄ : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) {x : DirectLimit G f | x ∈ A} = S
Tactic: rw [← image_univ, image_image, image_univ, ← eq_y,
    Subtype.range_coe_subtype, Finset.setOf_mem, A_closure]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
h :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' y '' univ) =
    S
h₁ :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (x : ↥A) ↦ ⟦Structure.Sigma.mk (G := G) f i (y x)⟧) '' univ) =
    S
h₂ :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      (range fun (x : ↥A) ↦ ⟦Structure.Sigma.mk (G := G) f i (y x)⟧) =
    S
h₃ : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (range fun (a : ↥A) ↦ (↑a : DirectLimit G f)) = S
h₄ : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) {x : DirectLimit G f | x ∈ A} = S
h₅ : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
⊢ LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' range y) =
    S
have h₆ : S = S
Tactic: rw [← image_univ, image_image, image_univ, ← eq_y,
    Subtype.range_coe_subtype, Finset.setOf_mem, A_closure]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
P : Type u₁
inst_5 : L.Structure P
g : (i : ι) → Embedding.{u_1, u_2, w, u₁} L (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u₁ + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
x y : Σˣ (G := G) f
xy : x ≈ y
⊢ Eq.{u₁ + 1} (α := P) ((g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) : P)
    ((g (y.fst (β := fun (i : ι) ↦ G i)) : (a : G y.fst) → P) (y.snd (β := fun (i : ι) ↦ G i)) : P)
have obtain : ∀ (i : ι) (hx : x.fst (β := fun (i : ι) ↦ G i) ≤ i) (hy : y.fst (β := fun (i : ι) ↦ G i) ≤ i),
  Eq.{u₁ + 1} (α := P) ((g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) : P)
    ((g (y.fst (β := fun (i : ι) ↦ G i)) : (a : G y.fst) → P) (y.snd (β := fun (i : ι) ↦ G i)) : P)
Tactic: obtain ⟨i, hx, hy⟩ := directed_of (· ≤ ·) x.1 y.1