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)
x y : Σˣ (G := G) f
i : ι
hx : x.fst (β := fun (i : ι) ↦ G i) ≤ i
hy : y.fst (β := fun (i : ι) ↦ G i) ≤ i
⊢ x ≈ y ↔
    Eq (α := G i)
      ((f (x.fst (β := fun (i : ι) ↦ G i)) i hx : (a : G x.fst) → G i) (x.snd (β := fun (i : ι) ↦ G i)) : G i)
      ((f (y.fst (β := fun (i : ι) ↦ G i)) i hy : (a : G y.fst) → G i) (y.snd (β := fun (i : ι) ↦ G i)) : G i)
have mk : ∀ (fst : ι) (snd : G fst) (hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i),
  Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ y ↔
    Eq (α := G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
            (a : G ⟨fst, snd⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
        G i)
      ((f (y.fst (β := fun (i : ι) ↦ G i)) i hy : (a : G y.fst) → G i) (y.snd (β := fun (i : ι) ↦ G i)) : G i)
Tactic: cases x
Cleared hypotheses: x, hx
-- 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)
y : Σˣ (G := G) f
i : ι
hy : y.fst (β := fun (i : ι) ↦ G i) ≤ i
fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
⊢ Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ y ↔
    Eq (α := G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
            (a : G ⟨fst, snd⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
        G i)
      ((f (y.fst (β := fun (i : ι) ↦ G i)) i hy : (a : G y.fst) → G i) (y.snd (β := fun (i : ι) ↦ G i)) : G i)
have mk : ∀ (fst_1 : ι) (snd_1 : G fst_1) (hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i),
  Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1 ↔
    Eq (α := G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
            (a : G ⟨fst, snd⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
        G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
            (a : G ⟨fst_1, snd_1⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
        G i)
Tactic: cases y
Cleared hypotheses: y, 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)
i fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
fst_1 : ι
snd_1 : G fst_1
hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i
⊢ Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1 ↔
    Eq (α := G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
            (a : G ⟨fst, snd⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
        G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
            (a : G ⟨fst_1, snd_1⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
        G i)
have mk : ∀ (xy : Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1),
  Eq (α := G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G ⟨fst, snd⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
          (a : G ⟨fst_1, snd_1⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G i)
Tactic: refine ⟨fun xy => ?_, fun xy => ⟨i, hx, hy, 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)
i fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
fst_1 : ι
snd_1 : G fst_1
hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i
xy : Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1
⊢ Eq (α := G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G ⟨fst, snd⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
          (a : G ⟨fst_1, snd_1⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G i)
have mk : ∀ (j : ι) (w : fst ≤ j) (w_1 : fst_1 ≤ j)
  (h : Eq (α := G j) ((f fst j w : (a : G fst) → G j) snd : G j) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j)),
  Eq (α := G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G ⟨fst, snd⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
          (a : G ⟨fst_1, snd_1⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G i)
Tactic: obtain ⟨j, _, _, h⟩ := xy
Cleared hypotheses: 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)
i fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
fst_1 : ι
snd_1 : G fst_1
hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i
j : ι
w : fst ≤ j
w_1 : fst_1 ≤ j
h : Eq (α := G j) ((f fst j w : (a : G fst) → G j) snd : G j) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j)
⊢ Eq (α := G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G ⟨fst, snd⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
          (a : G ⟨fst_1, snd_1⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G i)
have mk : ∀ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
  Eq (α := G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G ⟨fst, snd⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
          (a : G ⟨fst_1, snd_1⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G i)
Tactic: obtain ⟨k, ik, jk⟩ := directed_of (· ≤ ·) i j
-- 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)
i fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
fst_1 : ι
snd_1 : G fst_1
hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i
j : ι
w : fst ≤ j
w_1 : fst_1 ≤ j
h : Eq (α := G j) ((f fst j w : (a : G fst) → G j) snd : G j) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j)
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ Eq (α := G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G ⟨fst, snd⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
          (a : G ⟨fst_1, snd_1⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G i)
have h₁ : Eq (α := G k) ((f j k jk : (a : G j) → G k) ((f fst j w : (a : G fst) → G j) snd : G j) : G k)
  ((f j k jk : (a : G j) → G k) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j) : G k)
Tactic: have h := congr_arg (f j k jk) 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)
i fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
fst_1 : ι
snd_1 : G fst_1
hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i
j : ι
w : fst ≤ j
w_1 : fst_1 ≤ j
h_1 : Eq (α := G j) ((f fst j w : (a : G fst) → G j) snd : G j) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j)
k : ι
ik : i ≤ k
jk : j ≤ k
h :
  Eq (α := G k) ((f j k jk : (a : G j) → G k) ((f fst j w : (a : G fst) → G j) snd : G j) : G k)
    ((f j k jk : (a : G j) → G k) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j) : G k)
⊢ Eq (α := G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G ⟨fst, snd⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
          (a : G ⟨fst_1, snd_1⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G i)
have mk : Eq (α := G k)
  ((f i k ik : (a : G i) → G k)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
            (a : G ⟨fst, snd⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
        G i) :
    G k)
  ((f i k ik : (a : G i) → G k)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
            (a : G ⟨fst_1, snd_1⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
        G i) :
    G k)
Tactic: apply (f i k ik).injective
-- 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)
i fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
fst_1 : ι
snd_1 : G fst_1
hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i
j : ι
w : fst ≤ j
w_1 : fst_1 ≤ j
h_1 : Eq (α := G j) ((f fst j w : (a : G fst) → G j) snd : G j) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j)
k : ι
ik : i ≤ k
jk : j ≤ k
h :
  Eq (α := G k) ((f j k jk : (a : G j) → G k) ((f fst j w : (a : G fst) → G j) snd : G j) : G k)
    ((f j k jk : (a : G j) → G k) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j) : G k)
⊢ Eq (α := G k)
    ((f i k ik : (a : G i) → G k)
        ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
              (a : G ⟨fst, snd⟩.fst) → G i)
            ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
          G i) :
      G k)
    ((f i k ik : (a : G i) → G k)
        ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
              (a : G ⟨fst_1, snd_1⟩.fst) → G i)
            ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
          G i) :
      G k)
have mk : ∀ (h : Eq (α := G k) ((f fst k sorry : (a : G fst) → G k) snd : G k) ((f fst_1 k sorry : (a : G fst_1) → G k) snd_1 : G k)),
  Eq (α := G k)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) k sorry : (a : G ⟨fst, snd⟩.fst) → G k)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G k)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) k sorry :
          (a : G ⟨fst_1, snd_1⟩.fst) → G k)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G k)
Tactic: rw [DirectedSystem.map_map, DirectedSystem.map_map] at *
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)
n : ℕ
F : L.Functions 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))
⊢ Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f x i hi)) ≈
    Structure.Sigma.mk (G := G) f j (funMap F (unify (G := G) f x j hj))
have obtain : ∀ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
  Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f x i hi)) ≈
    Structure.Sigma.mk (G := G) f j (funMap F (unify (G := G) f x j hj))
Tactic: obtain ⟨k, ik, jk⟩ := directed_of (· ≤ ·) i 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)
n : ℕ
F : L.Functions 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
⊢ Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f x i hi)) ≈
    Structure.Sigma.mk (G := G) f j (funMap F (unify (G := G) f x j hj))
have refine : Eq (α := G k) ((f i k ik : (a : G i) → G k) (funMap F (unify (G := G) f x i hi)) : G k)
  ((f j k jk : (a : G j) → G k) (funMap F (unify (G := G) f x j hj)) : G k)
Tactic: refine ⟨k, ik, jk, ?_⟩
-- 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 : ℕ
F : L.Functions 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
⊢ Eq (α := G k) ((f i k ik : (a : G i) → G k) (funMap F (unify (G := G) f x i hi)) : G k)
    ((f j k jk : (a : G j) → G k) (funMap F (unify (G := G) f x j hj)) : G k)
have rw : Eq (α := G k) (funMap F ((⇑(f i k ik) : (a : G i) → G k) ∘ unify (G := G) f x i hi) : G k)
  ((f j k jk : (a : G j) → G k) (funMap F (unify (G := G) f x j hj)) : G k)
Tactic: rw [(f i k ik).map_fun, (f j k jk).map_fun, comp_unify, 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)
n : ℕ
F : L.Functions 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 :
  Eq (α := G k) (funMap F ((⇑(f i k ik) : (a : G i) → G k) ∘ unify (G := G) f x i hi) : G k)
    ((f j k jk : (a : G j) → G k) (funMap F (unify (G := G) f x j hj)) : G k)
⊢ Eq (α := G k) ((f i k ik : (a : G i) → G k) (funMap F (unify (G := G) f x i hi)) : G k)
    ((f j k jk : (a : G j) → G k) (funMap F (unify (G := G) f x j hj)) : G k)
have rw₁ : Eq (α := G k) (funMap F ((⇑(f i k ik) : (a : G i) → G k) ∘ unify (G := G) f x i hi))
  (funMap F ((⇑(f j k jk) : (a : G j) → G k) ∘ unify (G := G) f x j hj))
Tactic: rw [(f i k ik).map_fun, (f j k jk).map_fun, comp_unify, 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)
n : ℕ
F : L.Functions 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 :
  Eq (α := G k) (funMap F ((⇑(f i k ik) : (a : G i) → G k) ∘ unify (G := G) f x i hi) : G k)
    ((f j k jk : (a : G j) → G k) (funMap F (unify (G := G) f x j hj)) : G k)
rw₁ :
  Eq (α := G k) (funMap F ((⇑(f i k ik) : (a : G i) → G k) ∘ unify (G := G) f x i hi))
    (funMap F ((⇑(f j k jk) : (a : G j) → G k) ∘ unify (G := G) f x j hj))
⊢ Eq (α := G k) ((f i k ik : (a : G i) → G k) (funMap F (unify (G := G) f x i hi)) : G k)
    ((f j k jk : (a : G j) → G k) (funMap F (unify (G := G) f x j hj)) : G k)
have rw₂ : funMap F (unify (G := G) f x k sorry) = funMap F ((⇑(f j k jk) : (a : G j) → G k) ∘ unify (G := G) f x j hj)
Tactic: rw [(f i k ik).map_fun, (f j k jk).map_fun, comp_unify, 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)
n : ℕ
F : L.Functions 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 :
  Eq (α := G k) (funMap F ((⇑(f i k ik) : (a : G i) → G k) ∘ unify (G := G) f x i hi) : G k)
    ((f j k jk : (a : G j) → G k) (funMap F (unify (G := G) f x j hj)) : G k)
rw₁ :
  Eq (α := G k) (funMap F ((⇑(f i k ik) : (a : G i) → G k) ∘ unify (G := G) f x i hi))
    (funMap F ((⇑(f j k jk) : (a : G j) → G k) ∘ unify (G := G) f x j hj))
rw₂ : funMap F (unify (G := G) f x k ⋯) = funMap F ((⇑(f j k jk) : (a : G j) → G k) ∘ unify (G := G) f x j hj)
⊢ Eq (α := G k) ((f i k ik : (a : G i) → G k) (funMap F (unify (G := G) f x i hi)) : G k)
    ((f j k jk : (a : G j) → G k) (funMap F (unify (G := G) f x j hj)) : G k)
have rw₃ : funMap F (unify (G := G) f x k sorry) = funMap F (unify (G := G) f x k sorry)
Tactic: rw [(f i k ik).map_fun, (f j k jk).map_fun, comp_unify, 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)
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))
⊢ RelMap R (unify (G := G) f x i hi) = RelMap R (unify (G := G) f x j hj)
have obtain : ∀ (k : ι) (ik : i ≤ k) (jk : j ≤ k), RelMap R (unify (G := G) f x i hi) = RelMap R (unify (G := G) f x j hj)
Tactic: obtain ⟨k, ik, jk⟩ := directed_of (· ≤ ·) i 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)
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
⊢ RelMap R (unify (G := G) f x i hi) = RelMap R (unify (G := G) f x j hj)
have 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)
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_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)
⊢ 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 j hj)
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_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)
⊢ 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 (M := G k) R ((⇑(f j k jk) : (a : G j) → G k) ∘ unify (G := G) f x j hj)
Tactic: rw [← (f i k ik).map_rel, comp_unify, ← (f j k jk).map_rel, comp_unify]