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_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)
n : ℕ
R : L.Relations n
x : Fin n → Σˣ (G := G) f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
rw :
  RelMap (M := G k) R ((⇑(f i k ik) : (a : G i) → G k) ∘ unify (G := G) f x i hi) = RelMap R (unify (G := G) f x j hj)
rw₁ : RelMap R (unify (G := G) f x k ⋯) = RelMap R (unify (G := G) f x j hj)
rw₂ :
  RelMap R (unify (G := G) f x k ⋯) = RelMap (M := G k) R ((⇑(f j k jk) : (a : G j) → G k) ∘ unify (G := G) f x j hj)
⊢ RelMap R (unify (G := G) f x i hi) = RelMap R (unify (G := G) f x j hj)
have rw₃ : RelMap R (unify (G := G) f x k sorry) = RelMap R (unify (G := G) f x k sorry)
Tactic: rw [← (f i k ik).map_rel, comp_unify, ← (f j k jk).map_rel, comp_unify]
-- 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 y : α → Σˣ (G := G) f
xy : x ≈ y
⊢ ∃ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))) (hy :
    i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))), unify (G := G) f x i hx = unify (G := G) f y i hy
have obtain : ∀ (i : ι)
  (hi :
    Membership.mem (γ := Set ι)
      (upperBounds
        (range.{v, u_1 + 1} (ι := α ⊕ α)
          (Sum.elim (fun (a : α) ↦ (x a).fst (β := fun (i : ι) ↦ G i)) fun (a : α) ↦
            (y a).fst (β := fun (i : ι) ↦ G i))))
      i),
  ∃ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))) (hy :
    i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))), unify (G := G) f x i hx = unify (G := G) f y i hy
Tactic: obtain ⟨i, hi⟩ := Finite.bddAbove_range (Sum.elim (fun a => (x a).1) fun a => (y a).1)
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (hypothesis)
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 y : α → Σˣ (G := G) f
xy : x ≈ y
i : ι
hi :
  Membership.mem (γ := Set ι)
    (upperBounds
      (range.{v, u_1 + 1} (ι := α ⊕ α)
        (Sum.elim (fun (a : α) ↦ (x a).fst (β := fun (i : ι) ↦ G i)) fun (a : α) ↦ (y a).fst (β := fun (i : ι) ↦ G i))))
    i
⊢ ∃ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))) (hy :
    i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))), unify (G := G) f x i hx = unify (G := G) f y i hy
have hi₁ : Membership.mem (γ := Set ι)
  (upperBounds (range fun (a : α) ↦ (x a).fst (β := fun (i : ι) ↦ G i)) ∩
    upperBounds (range fun (a : α) ↦ (y a).fst (β := fun (i : ι) ↦ G i)))
  i
Tactic: rw [Sum.elim_range, upperBounds_union] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (hypothesis)
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 y : α → Σˣ (G := G) f
xy : x ≈ y
i : ι
hi :
  Membership.mem (γ := Set ι)
    (upperBounds (range fun (a : α) ↦ (x a).fst (β := fun (i : ι) ↦ G i)) ∩
      upperBounds (range fun (a : α) ↦ (y a).fst (β := fun (i : ι) ↦ G i)))
    i
⊢ ∃ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))) (hy :
    i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))), unify (G := G) f x i hx = unify (G := G) f y i hy
have hi₁ : Membership.mem (γ := Set ι)
  (upperBounds (range fun (a : α) ↦ (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x) a) ∩
    upperBounds (range fun (a : α) ↦ (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y) a))
  i
Tactic: simp_rw [← Function.comp_apply (f := Sigma.fst)] at hi
Cleared hypotheses: hi
-- 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 ι
n : ℕ
F : L.Functions n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
⊢ funMap F x ≈ funMap F y
have obtain : ∀ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x)))
  (hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y)))
  (h : unify (G := G) f x i hx = unify (G := G) f y i hy), funMap F x ≈ funMap F y
Tactic: obtain ⟨i, hx, hy, h⟩ := exists_unify_eq G f xy
-- 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 ι
n : ℕ
F : L.Functions n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))
h : unify (G := G) f x i hx = unify (G := G) f y i hy
⊢ funMap F x ≈ funMap F y
have G₁ : Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f x i hx)) ≈
  Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f y i hy))
Tactic: refine
      Setoid.trans (funMap_equiv_unify G f F x i hx)
        (Setoid.trans ?_ (Setoid.symm (funMap_equiv_unify G f F y i hy)))
-- 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 ι
n : ℕ
F : L.Functions n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))
h : unify (G := G) f x i hx = unify (G := G) f y i hy
⊢ Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f x i hx)) ≈
    Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f y i hy))
have rw : (setoid G f : Σˣ f → Σˣ f → Prop) (Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f y i hy)))
  (Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f y i hy)))
Tactic: rw [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 ι
n : ℕ
R : L.Relations n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
⊢ RelMap R x = RelMap R y
have obtain : ∀ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x)))
  (hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y)))
  (h : unify (G := G) f x i hx = unify (G := G) f y i hy), RelMap R x = RelMap R y
Tactic: obtain ⟨i, hx, hy, h⟩ := exists_unify_eq G f xy
-- 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 ι
n : ℕ
R : L.Relations n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))
h : unify (G := G) f x i hx = unify (G := G) f y i hy
⊢ RelMap R x = RelMap R y
have refine : RelMap R (unify (G := G) f x i hx) = RelMap R (unify (G := G) f y i hy)
Tactic: refine _root_.trans (relMap_equiv_unify G f R x i hx)
      (_root_.trans ?_ (symm (relMap_equiv_unify G f R y i hy)))
-- 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 ι
n : ℕ
R : L.Relations n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))
h : unify (G := G) f x i hx = unify (G := G) f y i hy
⊢ RelMap R (unify (G := G) f x i hx) = RelMap R (unify (G := G) f y i hy)
have rw : RelMap R (unify (G := G) f y i hy) = RelMap R (unify (G := G) f y i hy)
Tactic: rw [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 ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
⊢ (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (x a)⟧) = ⟦Structure.Sigma.mk (G := G) f i (funMap F x)⟧
have simp : (setoid G f : Σˣ f → Σˣ f → Prop) (funMap F fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
  (Structure.Sigma.mk (G := G) f i (funMap F x))
Tactic: simp only [funMap_quotient_mk', 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 ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
⊢ (setoid G f : Σˣ f → Σˣ f → Prop) (funMap F fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
    (Structure.Sigma.mk (G := G) f i (funMap F x))
have obtain : ∀ (k : ι) (ik : i ≤ k)
  (jk : Classical.choose (p := Membership.mem (γ := Set ι) (upperBounds (range fun (x : Fin n) ↦ i))) sorry ≤ k),
  (setoid G f : Σˣ f → Σˣ f → Prop) (funMap F fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
    (Structure.Sigma.mk (G := G) f i (funMap F x))
Tactic: obtain ⟨k, ik, jk⟩ :=
    directed_of (· ≤ ·) i (Classical.choose (Finite.bddAbove_range fun _ : Fin n => 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 ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
k : ι
ik : i ≤ k
jk : Classical.choose (p := Membership.mem (γ := Set ι) (upperBounds (range fun (x : Fin n) ↦ i))) ⋯ ≤ k
⊢ (setoid G f : Σˣ f → Σˣ f → Prop) (funMap F fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
    (Structure.Sigma.mk (G := G) f i (funMap F x))
have refine : Eq (α := G k)
  ((f
          (Classical.choose (p :=
            Membership.mem (γ := Set ι)
              (upperBounds
                (range fun (a : Fin n) ↦
                  Sigma.fst (β := fun (i : ι) ↦ G i)
                    ((fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) a))))
            sorry)
          k jk :
        (a : G (Classical.choose sorry)) → G k)
      (funMap F
          (unify (G := G) f (fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
            (Classical.choose (p :=
              Membership.mem (γ := Set ι)
                (upperBounds
                  (range fun (a : Fin n) ↦
                    Sigma.fst (β := fun (i : ι) ↦ G i)
                      ((fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) a))))
              sorry)
            sorry) :
        G
          (Classical.choose (p :=
            Membership.mem (γ := Set ι)
              (upperBounds
                (range fun (a : Fin n) ↦
                  Sigma.fst (β := fun (i : ι) ↦ G i)
                    ((fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) a))))
            sorry)) :
    G k)
  ((f i k ik : (a : G i) → G k) (funMap F x) : G k)
Tactic: refine ⟨k, jk, ik, ?_⟩
-- 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 ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
k : ι
ik : i ≤ k
jk : Classical.choose (p := Membership.mem (γ := Set ι) (upperBounds (range fun (x : Fin n) ↦ i))) ⋯ ≤ k
⊢ Eq (α := G k)
    ((f
            (Classical.choose (p :=
              Membership.mem (γ := Set ι)
                (upperBounds
                  (range fun (a : Fin n) ↦
                    Sigma.fst (β := fun (i : ι) ↦ G i)
                      ((fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) a))))
              ⋯)
            k jk :
          (a : G (Classical.choose ⋯)) → G k)
        (funMap F
            (unify (G := G) f (fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
              (Classical.choose (p :=
                Membership.mem (γ := Set ι)
                  (upperBounds
                    (range fun (a : Fin n) ↦
                      Sigma.fst (β := fun (i : ι) ↦ G i)
                        ((fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) a))))
                ⋯)
              ⋯) :
          G
            (Classical.choose (p :=
              Membership.mem (γ := Set ι)
                (upperBounds
                  (range fun (a : Fin n) ↦
                    Sigma.fst (β := fun (i : ι) ↦ G i)
                      ((fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) a))))
              ⋯)) :
      G k)
    ((f i k ik : (a : G i) → G k) (funMap F x) : G k)
have simp : funMap F (unify (G := G) f (fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) k sorry) =
  funMap F ((⇑(f i k ik) : (a : G i) → G k) ∘ x)
Tactic: simp only [Embedding.map_fun, comp_unify]
-- 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 ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
⊢ (RelMap (M := Quotient (setoid G f)) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (x a)⟧) = RelMap R x
have rw : (RelMap (M := Σˣ (G := G) f) R fun (a : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x a)) = RelMap R x
Tactic: rw [relMap_quotient_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 ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
⊢ (RelMap (M := Σˣ (G := G) f) R fun (a : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x a)) = RelMap R x
have rw : RelMap R (unify (G := G) f (fun (a : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x a)) i sorry) = RelMap R x
Tactic: rw [relMap_equiv_unify G f R (fun a => .mk f i (x a)) i (fun _ ⟨_, hj⟩ => le_of_eq hj.symm)]
-- 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 ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
⊢ RelMap R (unify (G := G) f (fun (a : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x a)) i ⋯) = RelMap R x
have rw : RelMap R x = RelMap R x
Tactic: rw [unify_sigma_mk_self]
-- 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 : ι) (y : α → G i), x = fun (a : α) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
have obtain : ∀ (i : ι)
  (hi :
    Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)))
      i),
  ∃ (i : ι) (y : α → G i), x = fun (a : α) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
Tactic: obtain ⟨i, hi⟩ := Finite.bddAbove_range fun a => (x a).out.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_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
⊢ ∃ (i : ι) (y : α → G i), x = fun (a : α) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
have refine : x = fun (a : α) ↦ ⟦Structure.Sigma.mk (G := G) f i (unify (G := G) f (Quotient.out ∘ x) i hi a)⟧
Tactic: refine ⟨i, unify f (Quotient.out ∘ x) i hi, ?_⟩
-- 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
⊢ x = fun (a : α) ↦ ⟦Structure.Sigma.mk (G := G) f i (unify (G := G) f (Quotient.out ∘ x) i hi a)⟧
have h : ∀ (a : α), x a = ⟦Structure.Sigma.mk (G := G) f i (unify (G := G) f (Quotient.out ∘ x) i hi a)⟧
Tactic: ext a
-- 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 : α
⊢ x a = ⟦Structure.Sigma.mk (G := G) f i (unify (G := G) f (Quotient.out ∘ x) i hi a)⟧
have h : Quotient.out (x a) ≈
  Structure.Sigma.mk (G := G) f 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)))
Tactic: rw [Quotient.eq_mk_iff_out, unify]
-- 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 : α
⊢ Quotient.out (x a) ≈
    Structure.Sigma.mk (G := G) f 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)))
have h : ∀ (r : ((Quotient.out ∘ x) a).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)))
Tactic: generalize_proofs r
-- 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
⊢ 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 : 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)))
Tactic: change _ ≈ Structure.Sigma.mk f i (f (Quotient.out (x a)).fst i r (Quotient.out (x a)).snd)
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (hypothesis)
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
⊢ 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 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
Tactic: have : (.mk f i (f (Quotient.out (x a)).fst i r (Quotient.out (x a)).snd) : Σˣ f).fst ≤ i :=
    le_rfl