awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih :
  ∀ (h : m ≤ m + k),
    (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
      Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
h : m ≤ m + (k + 1)
h₁ :
  Eq (α := G' (m + (k + 1)))
    ((natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x : G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
h₂ :
  Eq (α := G' (m + (k + 1)))
    (((Nat.leRecOn (C := fun (x : ℕ) ↦ G' m ↪[L] G' x) h (fun (k : ℕ) (g : G' m ↪[L] G' k) ↦ (f' k).comp g)
              (Embedding.refl L (G' m)) :
            G' m ↪[L] G' (m + (k + 1))) :
          (a : G' m) → G' (m + (k + 1)))
        x :
      G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
h₃ :
  Eq (α := G' (m + (k + 1)))
    ((Embedding.comp (f' (m + k))
            (Nat.leRecOn (C := fun (x : ℕ) ↦ G' m ↪[L] G' x) (n := m) (m := m + k) ⋯
              (fun {k : ℕ} (g : G' m ↪[L] G' k) ↦ (f' k).comp g) (Embedding.refl L (G' m))) :
          (a : G' m) → G' (m + (k + 1)))
        x :
      G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
⊢ (natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
have h₄ : Eq (α := G' (m + (k + 1)))
  ((Embedding.comp (f' (m + k)) (natLERec (G' := G') f' m (m + k) sorry) : (a : G' m) → G' (m + (k + 1))) x :
    G' (m + (k + 1)))
  ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
      (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) sorry (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
    G' (m + k + 1))
Tactic: rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
      Embedding.comp_apply, ih]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih :
  ∀ (h : m ≤ m + k),
    (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
      Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
h : m ≤ m + (k + 1)
h₁ :
  Eq (α := G' (m + (k + 1)))
    ((natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x : G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
h₂ :
  Eq (α := G' (m + (k + 1)))
    (((Nat.leRecOn (C := fun (x : ℕ) ↦ G' m ↪[L] G' x) h (fun (k : ℕ) (g : G' m ↪[L] G' k) ↦ (f' k).comp g)
              (Embedding.refl L (G' m)) :
            G' m ↪[L] G' (m + (k + 1))) :
          (a : G' m) → G' (m + (k + 1)))
        x :
      G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
h₃ :
  Eq (α := G' (m + (k + 1)))
    ((Embedding.comp (f' (m + k))
            (Nat.leRecOn (C := fun (x : ℕ) ↦ G' m ↪[L] G' x) (n := m) (m := m + k) ⋯
              (fun {k : ℕ} (g : G' m ↪[L] G' k) ↦ (f' k).comp g) (Embedding.refl L (G' m))) :
          (a : G' m) → G' (m + (k + 1)))
        x :
      G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
h₄ :
  Eq (α := G' (m + (k + 1)))
    ((Embedding.comp (f' (m + k)) (natLERec (G' := G') f' m (m + k) ⋯) : (a : G' m) → G' (m + (k + 1))) x :
      G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
⊢ (natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
have h₅ : Eq (α := G' (m + (k + 1)))
  ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
      ((natLERec (G' := G') f' m (m + k) sorry : (a : G' m) → G' (m + k)) x : G' (m + k)) :
    G' (m + k + 1))
  ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
      (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) sorry (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
    G' (m + k + 1))
Tactic: rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
      Embedding.comp_apply, ih]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih :
  ∀ (h : m ≤ m + k),
    (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
      Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
h : m ≤ m + (k + 1)
h₁ :
  Eq (α := G' (m + (k + 1)))
    ((natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x : G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
h₂ :
  Eq (α := G' (m + (k + 1)))
    (((Nat.leRecOn (C := fun (x : ℕ) ↦ G' m ↪[L] G' x) h (fun (k : ℕ) (g : G' m ↪[L] G' k) ↦ (f' k).comp g)
              (Embedding.refl L (G' m)) :
            G' m ↪[L] G' (m + (k + 1))) :
          (a : G' m) → G' (m + (k + 1)))
        x :
      G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
h₃ :
  Eq (α := G' (m + (k + 1)))
    ((Embedding.comp (f' (m + k))
            (Nat.leRecOn (C := fun (x : ℕ) ↦ G' m ↪[L] G' x) (n := m) (m := m + k) ⋯
              (fun {k : ℕ} (g : G' m ↪[L] G' k) ↦ (f' k).comp g) (Embedding.refl L (G' m))) :
          (a : G' m) → G' (m + (k + 1)))
        x :
      G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
h₄ :
  Eq (α := G' (m + (k + 1)))
    ((Embedding.comp (f' (m + k)) (natLERec (G' := G') f' m (m + k) ⋯) : (a : G' m) → G' (m + (k + 1))) x :
      G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
h₅ :
  Eq (α := G' (m + (k + 1)))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        ((natLERec (G' := G') f' m (m + k) ⋯ : (a : G' m) → G' (m + k)) x : G' (m + k)) :
      G' (m + k + 1))
    ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
        (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) ⋯ (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
      G' (m + k + 1))
⊢ (natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
have h₆ : Eq (α := G' (m + (k + 1)))
  ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
      (Nat.leRecOn (C := G') sorry (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
    G' (m + k + 1))
  ((f' (m + k) : (a : G' (m + k)) → G' (m + k + 1))
      (Nat.leRecOn (C := fun (x : ℕ) ↦ G' x) sorry (fun {k : ℕ} ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x) :
    G' (m + k + 1))
Tactic: rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
      Embedding.comp_apply, ih]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m k : ℕ
h : m ≤ m + k
x : G' m
⊢ (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
have h₁ : ∀ (h : m ≤ m + 0),
  (natLERec (G' := G') f' m (m + 0) h : (a : G' m) → G' (m + 0)) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
Tactic: induction k with
  | zero => simp [natLERec, Nat.leRecOn_self]
  | succ k ih =>
    rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
      Embedding.comp_apply, ih]
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m k : ℕ
h : m ≤ m + k
x : G' m
h₁ :
  ∀ (h : m ≤ m + 0),
    (natLERec (G' := G') f' m (m + 0) h : (a : G' m) → G' (m + 0)) x =
      Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
⊢ (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
have h₂ : ∀ (k : ℕ)
  (ih :
    ∀ (h : m ≤ m + k),
      (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
        Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x)
  (h : m ≤ m + (k + 1)),
  (natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
Tactic: induction k with
  | zero => simp [natLERec, Nat.leRecOn_self]
  | succ k ih =>
    rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
      Embedding.comp_apply, ih]
Cleared hypotheses: k, 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_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
α : Type u_1
i : ι
x : α → G i
⊢ unify (G := G) f (fun (a : α) ↦ Structure.Sigma.mk (G := G) f i (x a)) i ⋯ = x
have h : ∀ (a : α), unify (G := G) f (fun (a : α) ↦ Structure.Sigma.mk (G := G) f i (x a)) i sorry a = x 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
α : Type u_1
i : ι
x : α → G i
a : α
⊢ unify (G := G) f (fun (a : α) ↦ Structure.Sigma.mk (G := G) f i (x a)) i ⋯ a = x a
have h : ((f ((Structure.Sigma.mk (G := G) f i (x a)).fst (β := fun (i : ι) ↦ G i)) i sorry :
        G ((Structure.Sigma.mk (G := G) f i (x a)).fst (β := fun (i : ι) ↦ G i)) ↪[L] G i) :
      (a : G (Structure.Sigma.mk f i (x a)).fst) → G i)
    ((Structure.Sigma.mk (G := G) f i (x a)).snd (β := fun (i : ι) ↦ G i)) =
  x a
Tactic: rw [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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
α : Type u_1
x : α → Σˣ (G := G) f
i j : ι
ij : i ≤ j
h : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
⊢ (⇑(f i j ij) : (a : G i) → G j) ∘ unify (G := G) f x i h = unify (G := G) f x j ⋯
have h₁ : ∀ (a : α), ((⇑(f i j ij) : (a : G i) → G j) ∘ unify (G := G) f x i h) a = unify (G := G) f x j sorry 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_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
x_1 x_2 x_3 : Σˣ (G := G) f
i : ι
x : G i
j : ι
y : G j
h :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
k : ι
z : G k
h_1 :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : Eq (α := G ij) ((f i ij hiij : (a : G i) → G ij) x : G ij) ((f j ij hjij : (a : G j) → G ij) y : G ij)
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : Eq (α := G jk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) ((f k jk hkjk : (a : G k) → G jk) z : G jk)
⊢ match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
have obtain : ∀ (ijk : ι) (hijijk : ij ≤ ijk) (hjkijk : jk ≤ ijk),
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
Tactic: obtain ⟨ijk, hijijk, hjkijk⟩ := directed_of (· ≤ ·) ij 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
x_1 x_2 x_3 : Σˣ (G := G) f
i : ι
x : G i
j : ι
y : G j
h :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
k : ι
z : G k
h_1 :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : Eq (α := G ij) ((f i ij hiij : (a : G i) → G ij) x : G ij) ((f j ij hjij : (a : G j) → G ij) y : G ij)
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : Eq (α := G jk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) ((f k jk hkjk : (a : G k) → G jk) z : G jk)
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
⊢ match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
have refine : Eq (α := G ijk) ((f i ijk sorry : (a : G i) → G ijk) x : G ijk) ((f k ijk sorry : (a : G k) → G ijk) z : G ijk)
Tactic: refine ⟨ijk, le_trans hiij hijijk, le_trans hkjk hjkijk, ?_⟩
-- 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
x_1 x_2 x_3 : Σˣ (G := G) f
i : ι
x : G i
j : ι
y : G j
h :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
k : ι
z : G k
h_1 :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : Eq (α := G ij) ((f i ij hiij : (a : G i) → G ij) x : G ij) ((f j ij hjij : (a : G j) → G ij) y : G ij)
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : Eq (α := G jk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) ((f k jk hkjk : (a : G k) → G jk) z : G jk)
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
⊢ Eq (α := G ijk) ((f i ijk ⋯ : (a : G i) → G ijk) x : G ijk) ((f k ijk ⋯ : (a : G k) → G ijk) z : G ijk)
have rw : Eq (α := G ijk) ((f j ijk sorry : (a : G j) → G ijk) y : G ijk) ((f k ijk sorry : (a : G k) → G ijk) z : G ijk)
Tactic: rw [← DirectedSystem.map_map _ hiij hijijk, hij, DirectedSystem.map_map]
-- 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
x_1 x_2 x_3 : Σˣ (G := G) f
i : ι
x : G i
j : ι
y : G j
h :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
k : ι
z : G k
h_1 :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : Eq (α := G ij) ((f i ij hiij : (a : G i) → G ij) x : G ij) ((f j ij hjij : (a : G j) → G ij) y : G ij)
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : Eq (α := G jk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) ((f k jk hkjk : (a : G k) → G jk) z : G jk)
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
⊢ Eq (α := G ijk) ((f j ijk ⋯ : (a : G j) → G ijk) y : G ijk) ((f k ijk ⋯ : (a : G k) → G ijk) z : G ijk)
have rw : Eq (α := G ijk) ((f j ijk sorry : (a : G j) → G ijk) y : G ijk)
  ((f jk ijk hjkijk : (a : G jk) → G ijk) ((f k jk hkjk : (a : G k) → G jk) z : G jk) : G ijk)
Tactic: rw [← DirectedSystem.map_map _ hkjk hjkijk, ← hjk, DirectedSystem.map_map]
-- 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
x_1 x_2 x_3 : Σˣ (G := G) f
i : ι
x : G i
j : ι
y : G j
h :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
k : ι
z : G k
h_1 :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : Eq (α := G ij) ((f i ij hiij : (a : G i) → G ij) x : G ij) ((f j ij hjij : (a : G j) → G ij) y : G ij)
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : Eq (α := G jk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) ((f k jk hkjk : (a : G k) → G jk) z : G jk)
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
rw :
  Eq (α := G ijk) ((f j ijk ⋯ : (a : G j) → G ijk) y : G ijk)
    ((f jk ijk hjkijk : (a : G jk) → G ijk) ((f k jk hkjk : (a : G k) → G jk) z : G jk) : G ijk)
⊢ Eq (α := G ijk) ((f j ijk ⋯ : (a : G j) → G ijk) y : G ijk) ((f k ijk ⋯ : (a : G k) → G ijk) z : G ijk)
have rw₁ : Eq (α := G ijk) ((f j ijk sorry : (a : G j) → G ijk) y : G ijk)
  ((f jk ijk hjkijk : (a : G jk) → G ijk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) : G ijk)
Tactic: rw [← DirectedSystem.map_map _ hkjk hjkijk, ← hjk, DirectedSystem.map_map]
-- 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
x_1 x_2 x_3 : Σˣ (G := G) f
i : ι
x : G i
j : ι
y : G j
h :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
k : ι
z : G k
h_1 :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : Eq (α := G ij) ((f i ij hiij : (a : G i) → G ij) x : G ij) ((f j ij hjij : (a : G j) → G ij) y : G ij)
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : Eq (α := G jk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) ((f k jk hkjk : (a : G k) → G jk) z : G jk)
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
rw :
  Eq (α := G ijk) ((f j ijk ⋯ : (a : G j) → G ijk) y : G ijk)
    ((f jk ijk hjkijk : (a : G jk) → G ijk) ((f k jk hkjk : (a : G k) → G jk) z : G jk) : G ijk)
rw₁ :
  Eq (α := G ijk) ((f j ijk ⋯ : (a : G j) → G ijk) y : G ijk)
    ((f jk ijk hjkijk : (a : G jk) → G ijk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) : G ijk)
⊢ Eq (α := G ijk) ((f j ijk ⋯ : (a : G j) → G ijk) y : G ijk) ((f k ijk ⋯ : (a : G k) → G ijk) z : G ijk)
have rw₂ : Eq (α := G ijk) ((f j ijk sorry : (a : G j) → G ijk) y : G ijk) ((f j ijk sorry : (a : G j) → G ijk) y : G ijk)
Tactic: rw [← DirectedSystem.map_map _ hkjk hjkijk, ← hjk, DirectedSystem.map_map]