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)
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
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)
have rw : Eq.{u₁ + 1} (α := P)
  ((g i : (a : G i) → P)
      ((f (x.fst (β := fun (i : ι) ↦ G i)) i hx : (a : G x.fst) → G i) (x.snd (β := fun (i : ι) ↦ G i)) : G i) :
    P)
  ((g i : (a : G i) → P)
      ((f (y.fst (β := fun (i : ι) ↦ G i)) i hy : (a : G y.fst) → G i) (y.snd (β := fun (i : ι) ↦ G i)) : G i) :
    P)
Tactic: rw [← Hg x.1 i hx, ← Hg y.1 i hy]
-- 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 ι
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 : DirectLimit G f
xy :
  Eq.{u₁ + 1} (α := P)
    (Quotient.lift
      (fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⋯ x)
    (Quotient.lift
      (fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⋯ y)
⊢ x = y
have xy₁ : Eq.{u₁ + 1} (α := P)
  ((g ((Quotient.out x).fst (β := fun (i : ι) ↦ G i)) : (a : G (Quotient.out x).fst) → P)
      ((Quotient.out x).snd (β := fun (i : ι) ↦ G i)) :
    P)
  ((g ((Quotient.out y).fst (β := fun (i : ι) ↦ G i)) : (a : G (Quotient.out y).fst) → P)
      ((Quotient.out y).snd (β := fun (i : ι) ↦ G i)) :
    P)
Tactic: rw [← Quotient.out_eq x, ← Quotient.out_eq y, Quotient.lift_mk, Quotient.lift_mk] at 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)
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 : DirectLimit G f
xy :
  Eq.{u₁ + 1} (α := P)
    ((g ((Quotient.out x).fst (β := fun (i : ι) ↦ G i)) : (a : G (Quotient.out x).fst) → P)
        ((Quotient.out x).snd (β := fun (i : ι) ↦ G i)) :
      P)
    ((g ((Quotient.out y).fst (β := fun (i : ι) ↦ G i)) : (a : G (Quotient.out y).fst) → P)
        ((Quotient.out y).snd (β := fun (i : ι) ↦ G i)) :
      P)
⊢ x = y
have obtain : ∀ (i : ι) (hx : (Quotient.out x).fst (β := fun (i : ι) ↦ G i) ≤ i)
  (hy : (Quotient.out y).fst (β := fun (i : ι) ↦ G i) ≤ i), x = y
Tactic: obtain ⟨i, hx, hy⟩ := directed_of (· ≤ ·) x.out.1 y.out.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_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 : DirectLimit G f
xy :
  Eq.{u₁ + 1} (α := P)
    ((g ((Quotient.out x).fst (β := fun (i : ι) ↦ G i)) : (a : G (Quotient.out x).fst) → P)
        ((Quotient.out x).snd (β := fun (i : ι) ↦ G i)) :
      P)
    ((g ((Quotient.out y).fst (β := fun (i : ι) ↦ G i)) : (a : G (Quotient.out y).fst) → P)
        ((Quotient.out y).snd (β := fun (i : ι) ↦ G i)) :
      P)
i : ι
hx : (Quotient.out x).fst (β := fun (i : ι) ↦ G i) ≤ i
hy hy₁ : (Quotient.out y).fst (β := fun (i : ι) ↦ G i) ≤ i
⊢ x = y
have xy₁ : Eq.{u₁ + 1} (α := P)
  ((g i : (a : G i) → P)
      ((f ((Quotient.out x).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G (Quotient.out x).fst) → G i)
          ((Quotient.out x).snd (β := fun (i : ι) ↦ G i)) :
        G i) :
    P)
  ((g i : (a : G i) → P)
      ((f ((Quotient.out y).fst (β := fun (i : ι) ↦ G i)) i hy₁ : (a : G (Quotient.out y).fst) → G i)
          ((Quotient.out y).snd (β := fun (i : ι) ↦ G i)) :
        G i) :
    P)
Tactic: rw [← Hg x.out.1 i hx, ← Hg y.out.1 i hy] at xy
Cleared hypotheses: xy, 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 ι
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 : DirectLimit G f
i : ι
hx : (Quotient.out x).fst (β := fun (i : ι) ↦ G i) ≤ i
hy : (Quotient.out y).fst (β := fun (i : ι) ↦ G i) ≤ i
xy :
  Eq.{u₁ + 1} (α := P)
    ((g i : (a : G i) → P)
        ((f ((Quotient.out x).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G (Quotient.out x).fst) → G i)
            ((Quotient.out x).snd (β := fun (i : ι) ↦ G i)) :
          G i) :
      P)
    ((g i : (a : G i) → P)
        ((f ((Quotient.out y).fst (β := fun (i : ι) ↦ G i)) i hy : (a : G (Quotient.out y).fst) → G i)
            ((Quotient.out y).snd (β := fun (i : ι) ↦ G i)) :
          G i) :
      P)
⊢ x = y
have rw : Eq (α := G i)
  ((f ((Quotient.out x).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G (Quotient.out x).fst) → G i)
      ((Quotient.out x).snd (β := fun (i : ι) ↦ G i)) :
    G i)
  ((f ((Quotient.out y).fst (β := fun (i : ι) ↦ G i)) i hy : (a : G (Quotient.out y).fst) → G i)
      ((Quotient.out y).snd (β := fun (i : ι) ↦ G i)) :
    G i)
Tactic: rw [← Quotient.out_eq x, ← Quotient.out_eq y, Quotient.eq_iff_equiv, equiv_iff G f hx 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 ι
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)
n : ℕ
F : L.Functions n
x : Fin n → DirectLimit G f
⊢ Eq.{u₁ + 1} (α := P)
    (Quotient.lift
      (fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⋯ (funMap F x))
    (funMap F
      (Quotient.lift
          (fun (x : Σˣ (G := G) f) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
          ⋯ ∘
        x))
have obtain : ∀ (i : ι) (y : Fin n → G i),
  Eq.{u₁ + 1} (α := P)
    (Quotient.lift (s := setoid G f)
      (fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      sorry (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧))
    (funMap F
      (Function.comp (β := DirectLimit G f)
        (Quotient.lift
          (fun (x : Σˣ (G := G) f) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
          sorry)
        fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧))
Tactic: obtain ⟨i, y, rfl⟩ := exists_quotient_mk'_sigma_mk'_eq G f x
Cleared hypotheses: x
-- 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)
n : ℕ
F : L.Functions n
i : ι
y : Fin n → G i
⊢ Eq.{u₁ + 1} (α := P)
    (Quotient.lift (s := setoid G f)
      (fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⋯ (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧))
    (funMap F
      (Function.comp (β := DirectLimit G f)
        (Quotient.lift
          (fun (x : Σˣ (G := G) f) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
          ⋯)
        fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧))
have change : Eq.{u₁ + 1} (α := P)
  (Quotient.lift (s := setoid G f)
    (fun (x : Σˣ (G := G) f) ↦
      (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
    sorry (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧))
  (funMap F
    (Quotient.lift
        (fun (x : Σˣ (G := G) f) ↦
          (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
        sorry ∘
      Quotient.mk (setoid G f) ∘ Structure.Sigma.mk (G := G) f i ∘ y))
Tactic: change _ = funMap F (Quotient.lift _ _ ∘ Quotient.mk _ ∘ Structure.Sigma.mk f i ∘ 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 ι
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)
n : ℕ
F : L.Functions n
i : ι
y : Fin n → G i
⊢ Eq.{u₁ + 1} (α := P)
    (Quotient.lift (s := setoid G f)
      (fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⋯ (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧))
    (funMap F
      (Quotient.lift
          (fun (x : Σˣ (G := G) f) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
          ⋯ ∘
        Quotient.mk (setoid G f) ∘ Structure.Sigma.mk (G := G) f i ∘ y))
have rw : Eq.{u₁ + 1} (α := P)
  (Quotient.lift
    (fun (x : Σˣ (G := G) f) ↦
      (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
    sorry ⟦Structure.Sigma.mk (G := G) f i (funMap F y)⟧)
  (funMap F
    ((fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i))) ∘
      Structure.Sigma.mk (G := G) f i ∘ y))
Tactic: rw [funMap_quotient_mk'_sigma_mk', ← Function.comp_assoc, Quotient.lift_comp_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 ι
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)
n : ℕ
F : L.Functions n
i : ι
y : Fin n → G i
⊢ Eq.{u₁ + 1} (α := P)
    (Quotient.lift
      (fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⋯ ⟦Structure.Sigma.mk (G := G) f i (funMap F y)⟧)
    (funMap F
      ((fun (x : Σˣ (G := G) f) ↦
          (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i))) ∘
        Structure.Sigma.mk (G := G) f i ∘ y))
have simp : Eq.{u₁ + 1} (α := P) (funMap F ((⇑(g i) : (a : G i) → P) ∘ y))
  (funMap F
    ((fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i))) ∘
      Structure.Sigma.mk (G := G) f i ∘ y))
Tactic: simp only [Quotient.lift_mk, Embedding.map_fun]
-- 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)
n : ℕ
R : L.Relations n
x : Fin n → DirectLimit G f
⊢ RelMap.{u_1, u_2, u₁} (M := P) R
      (Quotient.lift
          (fun (x : Σˣ (G := G) f) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
          ⋯ ∘
        x) ↔
    RelMap R x
have obtain : ∀ (i : ι) (y : Fin n → G i),
  RelMap.{u_1, u_2, u₁} (M := P) R
      (Function.comp (β := DirectLimit G f)
        (Quotient.lift
          (fun (x : Σˣ (G := G) f) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
          sorry)
        fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧) ↔
    RelMap (M := DirectLimit G f) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
Tactic: obtain ⟨i, y, rfl⟩ := exists_quotient_mk'_sigma_mk'_eq G f x
Cleared hypotheses: x
-- 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)
n : ℕ
R : L.Relations n
i : ι
y : Fin n → G i
⊢ RelMap.{u_1, u_2, u₁} (M := P) R
      (Function.comp (β := DirectLimit G f)
        (Quotient.lift
          (fun (x : Σˣ (G := G) f) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
          ⋯)
        fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧) ↔
    RelMap (M := DirectLimit G f) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
have change : RelMap.{u_1, u_2, u₁} (M := P) R
    (Quotient.lift
        (fun (x : Σˣ (G := G) f) ↦
          (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
        sorry ∘
      Quotient.mk (setoid G f) ∘ Structure.Sigma.mk (G := G) f i ∘ y) ↔
  RelMap (M := DirectLimit G f) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
Tactic: change RelMap R (Quotient.lift _ _ ∘ Quotient.mk _ ∘ Structure.Sigma.mk f i ∘ 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 ι
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)
n : ℕ
R : L.Relations n
i : ι
y : Fin n → G i
⊢ RelMap.{u_1, u_2, u₁} (M := P) R
      (Quotient.lift
          (fun (x : Σˣ (G := G) f) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
          ⋯ ∘
        Quotient.mk (setoid G f) ∘ Structure.Sigma.mk (G := G) f i ∘ y) ↔
    RelMap (M := DirectLimit G f) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
have rw : RelMap.{u_1, u_2, u₁} (M := P) R
    ((fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i))) ∘
      Structure.Sigma.mk (G := G) f i ∘ y) ↔
  RelMap.{u_1, u_2, u₁} (M := P) R ((⇑(g i) : (a : G i) → P) ∘ y)
Tactic: rw [relMap_quotient_mk'_sigma_mk' G f, ← (g i).map_rel R y, ← Function.comp_assoc,
      Quotient.lift_comp_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 ι
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)
F : DirectLimit G f ↪[L] P
x_1 : DirectLimit G f
i j : ι
hij : i ≤ j
x : G i
⊢ Eq.{u₁ + 1} (α := P)
    (((fun (i : ι) ↦ F.comp (of L ι G f i)) j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
    (((fun (i : ι) ↦ F.comp (of L ι G f i)) i : (a : G i) → P) x : P)
have rw : Eq.{u₁ + 1} (α := P)
  ((F : (a : DirectLimit G f) → P)
      ((of L ι G f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G f) :
    P)
  (((fun (i : ι) ↦ F.comp (of L ι G f i)) i : (a : G i) → P) x : P)
Tactic: rw [F.comp_apply, F.comp_apply, of_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 ι
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)
F : DirectLimit G f ↪[L] P
x_1 : DirectLimit G f
i j : ι
hij : i ≤ j
x : G i
rw :
  Eq.{u₁ + 1} (α := P)
    ((F : (a : DirectLimit G f) → P)
        ((of L ι G f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G f) :
      P)
    (((fun (i : ι) ↦ F.comp (of L ι G f i)) i : (a : G i) → P) x : P)
⊢ Eq.{u₁ + 1} (α := P)
    (((fun (i : ι) ↦ F.comp (of L ι G f i)) j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
    (((fun (i : ι) ↦ F.comp (of L ι G f i)) i : (a : G i) → P) x : P)
have rw₁ : Eq.{u₁ + 1} (α := P)
  ((F : (a : DirectLimit G f) → P)
      ((of L ι G f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G f) :
    P)
  ((F : (a : DirectLimit G f) → P) ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
Tactic: rw [F.comp_apply, F.comp_apply, of_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 ι
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)
F : DirectLimit G f ↪[L] P
x_1 : DirectLimit G f
i j : ι
hij : i ≤ j
x : G i
rw :
  Eq.{u₁ + 1} (α := P)
    ((F : (a : DirectLimit G f) → P)
        ((of L ι G f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G f) :
      P)
    (((fun (i : ι) ↦ F.comp (of L ι G f i)) i : (a : G i) → P) x : P)
rw₁ :
  Eq.{u₁ + 1} (α := P)
    ((F : (a : DirectLimit G f) → P)
        ((of L ι G f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G f) :
      P)
    ((F : (a : DirectLimit G f) → P) ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
⊢ Eq.{u₁ + 1} (α := P)
    (((fun (i : ι) ↦ F.comp (of L ι G f i)) j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
    (((fun (i : ι) ↦ F.comp (of L ι G f i)) i : (a : G i) → P) x : P)
have rw₂ : Eq.{u₁ + 1} (α := P)
  ((F : (a : DirectLimit G f) → P) ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
  ((F : (a : DirectLimit G f) → P) ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
Tactic: rw [F.comp_apply, F.comp_apply, of_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 ι
P : Type u₁
inst_5 : L.Structure P
F : DirectLimit G f ↪[L] P
x_1 : DirectLimit G f
i : ι
x : G i
⊢ Eq.{u₁ + 1} (α := P)
    ((F : (a : DirectLimit G f) → P) ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
    ((lift L ι G f (fun (i : ι) ↦ F.comp (of L ι G f i)) ⋯ : (a : DirectLimit G f) → P)
        ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) :
      P)
have rw : Eq.{u₁ + 1} (α := P)
  ((F : (a : DirectLimit G f) → P) ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
  ((F.comp (of L ι G f i) : (a : G i) → P) x : P)
Tactic: rw [lift_of]