awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t :
  ∀ (y : Y),
    Eq (α := (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
          (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
          (fun (X : Type u) ↦ X) Z) →
      ∃! x : X, (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x = y
s : Fork g h
refine_1 : (i : s.pt) → (Fork.ofι f w).pt
⊢ { l : s.pt ⟶ (Fork.ofι f w).pt //
    l ≫ (Fork.ofι f w).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = l }
have refine_2 : (↾fun (i : s.pt) ↦
      Classical.choose (p := fun (x : X) ↦
        (fun (x : X) ↦
              Eq (α := (fun (X : Type u) ↦ X) Y)
                ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                  (fun (X : Type u) ↦ X) Y)
                ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
                  (fun (X : Type u) ↦ X) Y))
            x ∧
          ∀ (y : X),
            (fun (x : X) ↦
                  Eq (α := (fun (X : Type u) ↦ X) Y)
                    ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                      (fun (X : Type u) ↦ X) Y)
                    ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
                      (fun (X : Type u) ↦ X) Y))
                y →
              y = x)
        sorry) ≫
    (Fork.ofι f w).ι =
  s.ι
Tactic: refine ⟨↾fun i => ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t :
  ∀ (y : Y),
    Eq (α := (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
          (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
          (fun (X : Type u) ↦ X) Z) →
      ∃! x : X, (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x = y
s : Fork g h
refine_1 : (i : s.pt) → (Fork.ofι f w).pt
refine_2 :
  (↾fun (i : s.pt) ↦
        Classical.choose (p := fun (x : X) ↦
          (fun (x : X) ↦
                Eq (α := (fun (X : Type u) ↦ X) Y)
                  ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                    (fun (X : Type u) ↦ X) Y)
                  ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
                    (fun (X : Type u) ↦ X) Y))
              x ∧
            ∀ (y : X),
              (fun (x : X) ↦
                    Eq (α := (fun (X : Type u) ↦ X) Y)
                      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                        (fun (X : Type u) ↦ X) Y)
                      ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
                        (fun (X : Type u) ↦ X) Y))
                  y →
                y = x)
          ⋯) ≫
      (Fork.ofι f w).ι =
    s.ι
⊢ { l : s.pt ⟶ (Fork.ofι f w).pt //
    l ≫ (Fork.ofι f w).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = l }
have refine_3 : ∀ {m : s.pt ⟶ (Fork.ofι f w).pt},
  m ≫ (Fork.ofι f w).ι = s.ι →
    m =
      ↾fun (i : s.pt) ↦
        Classical.choose (p := fun (x : X) ↦
          (fun (x : X) ↦
                Eq (α := (fun (X : Type u) ↦ X) Y)
                  ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                    (fun (X : Type u) ↦ X) Y)
                  ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
                    (fun (X : Type u) ↦ X) Y))
              x ∧
            ∀ (y : X),
              (fun (x : X) ↦
                    Eq (α := (fun (X : Type u) ↦ X) Y)
                      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                        (fun (X : Type u) ↦ X) Y)
                      ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
                        (fun (X : Type u) ↦ X) Y))
                  y →
                y = x)
          sorry
Tactic: refine ⟨↾fun i => ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t :
  ∀ (y : Y),
    Eq (α := (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
          (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
          (fun (X : Type u) ↦ X) Z) →
      ∃! x : X, (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x = y
s : Fork g h
i : s.pt
⊢ (Fork.ofι f w).pt
have apply : Eq (α := (fun (X : Type u) ↦ X) Z)
  ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
      ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
        (fun (X : Type u) ↦ X) Y) :
    (fun (X : Type u) ↦ X) Z)
  ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
      ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
        (fun (X : Type u) ↦ X) Y) :
    (fun (X : Type u) ↦ X) Z)
Tactic: apply Classical.choose (t (s.ι i) _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t :
  ∀ (y : Y),
    Eq (α := (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
          (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
          (fun (X : Type u) ↦ X) Z) →
      ∃! x : X, (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x = y
s : Fork g h
⊢ (↾fun (i : s.pt) ↦
        Classical.choose (p := fun (x : X) ↦
          (fun (x : X) ↦
                Eq (α := (fun (X : Type u) ↦ X) Y)
                  ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                    (fun (X : Type u) ↦ X) Y)
                  ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
                    (fun (X : Type u) ↦ X) Y))
              x ∧
            ∀ (y : X),
              (fun (x : X) ↦
                    Eq (α := (fun (X : Type u) ↦ X) Y)
                      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                        (fun (X : Type u) ↦ X) Y)
                      ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
                        (fun (X : Type u) ↦ X) Y))
                  y →
                y = x)
          ⋯) ≫
      (Fork.ofι f w).ι =
    s.ι
have refine_2 : ∀ (i : s.pt),
  TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((↾fun (i : s.pt) ↦
            Classical.choose (p := fun (x : X) ↦
              (fun (x : X) ↦
                    Eq (α := (fun (X : Type u) ↦ X) Y)
                      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                        (fun (X : Type u) ↦ X) Y)
                      ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
                        (fun (X : Type u) ↦ X) Y))
                  x ∧
                ∀ (y : X),
                  (fun (x : X) ↦
                        Eq (α := (fun (X : Type u) ↦ X) Y)
                          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                            (fun (X : Type u) ↦ X) Y)
                          ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y)
                              i :
                            (fun (X : Type u) ↦ X) Y))
                      y →
                    y = x)
              sorry) ≫
          (Fork.ofι f w).ι))
      i =
    (hom (FC := TypeCat.Fun) s.ι).toFun i
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t :
  ∀ (y : Y),
    Eq (α := (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
          (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
          (fun (X : Type u) ↦ X) Z) →
      ∃! x : X, (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x = y
s : Fork g h
m : s.pt ⟶ (Fork.ofι f w).pt
hm : m ≫ (Fork.ofι f w).ι = s.ι
⊢ m =
    ↾fun (i : s.pt) ↦
      Classical.choose (p := fun (x : X) ↦
        (fun (x : X) ↦
              Eq (α := (fun (X : Type u) ↦ X) Y)
                ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                  (fun (X : Type u) ↦ X) Y)
                ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
                  (fun (X : Type u) ↦ X) Y))
            x ∧
          ∀ (y : X),
            (fun (x : X) ↦
                  Eq (α := (fun (X : Type u) ↦ X) Y)
                    ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                      (fun (X : Type u) ↦ X) Y)
                    ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
                      (fun (X : Type u) ↦ X) Y))
                y →
              y = x)
        ⋯
have refine_3 : ∀ (i : s.pt),
  (hom (FC := TypeCat.Fun) m).toFun i =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (↾fun (i : s.pt) ↦
          Classical.choose (p := fun (x : X) ↦
            (fun (x : X) ↦
                  Eq (α := (fun (X : Type u) ↦ X) Y)
                    ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                      (fun (X : Type u) ↦ X) Y)
                    ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
                      (fun (X : Type u) ↦ X) Y))
                x ∧
              ∀ (y : X),
                (fun (x : X) ↦
                      Eq (α := (fun (X : Type u) ↦ X) Y)
                        ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
                          (fun (X : Type u) ↦ X) Y)
                        ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y)
                            i :
                          (fun (X : Type u) ↦ X) Y))
                    y →
                  y = x)
            sorry))
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy :
  Eq (α := (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
y' : PUnit.{u + 1} ⟶ Y := ↾fun (x : PUnit.{u + 1}) ↦ y
⊢ y' ≫ g = y' ≫ h
have h₁ : ∀ (x : PUnit.{u + 1}), (hom (FC := TypeCat.Fun) (y' ≫ g)).toFun x = (hom (FC := TypeCat.Fun) (y' ≫ h)).toFun x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (hypothesis)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy :
  Eq (α := (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
y' : PUnit.{u + 1} ⟶ Y := ↾fun (x : PUnit.{u + 1}) ↦ y
⊢ ∃! x : X, (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x = y
have hy' : y' ≫ g = y' ≫ h
Tactic: have hy' : y' ≫ g = y' ≫ h := by ext; exact hy
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy :
  Eq (α := (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
y' : PUnit.{u + 1} ⟶ Y := ↾fun (x : PUnit.{u + 1}) ↦ y
hy' : y' ≫ g = y' ≫ h
⊢ ∃! x : X, (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x = y
have refine : ∀ (y_1 : X),
  (fun (x : X) ↦ (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x = y) y_1 →
    y_1 =
      (hom (FC := TypeCat.Fun) (↑(Fork.IsLimit.lift' t y' hy') : PUnit.{u + 1} ⟶ (Fork.ofι f w).pt) :
          (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (Fork.ofι f w).pt)
        PUnit.unit
Tactic: refine ⟨(Fork.IsLimit.lift' t _ hy').1 ⟨⟩, congr_hom (Fork.IsLimit.lift' t y' _).2 ⟨⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy :
  Eq (α := (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
y' : PUnit.{u + 1} ⟶ Y := ↾fun (x : PUnit.{u + 1}) ↦ y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x' = y
this :
  Eq (α := PUnit.{u + 1} → X) (fun (x : PUnit.{u + 1}) ↦ x')
    (⇑(hom (FC := TypeCat.Fun) (↑(Fork.IsLimit.lift' t y' hy') : PUnit.{u + 1} ⟶ (Fork.ofι f w).pt)) :
      (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (Fork.ofι f w).pt)
⊢ x' =
    (hom (FC := TypeCat.Fun) (↑(Fork.IsLimit.lift' t y' hy') : PUnit.{u + 1} ⟶ (Fork.ofι f w).pt) :
        (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (Fork.ofι f w).pt)
      PUnit.unit
have rw : x' = (fun (x : PUnit.{u + 1}) ↦ x') PUnit.unit
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy :
  Eq (α := (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
y' : PUnit.{u + 1} ⟶ Y := ↾fun (x : PUnit.{u + 1}) ↦ y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x' = y
⊢ x' =
    (hom (FC := TypeCat.Fun) (↑(Fork.IsLimit.lift' t y' hy') : PUnit.{u + 1} ⟶ (Fork.ofι f w).pt) :
        (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (Fork.ofι f w).pt)
      PUnit.unit
have suffices : Eq (α := PUnit.{u + 1} → X) (fun (x : PUnit.{u + 1}) ↦ x')
  (⇑(hom (FC := TypeCat.Fun) (↑(Fork.IsLimit.lift' t y' hy') : PUnit.{u + 1} ⟶ (Fork.ofι f w).pt)) :
    (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (Fork.ofι f w).pt)
Tactic: suffices (fun _ : PUnit => x') = (Fork.IsLimit.lift' t y' hy').1 by
    rw [← this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy :
  Eq (α := (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
y' : PUnit.{u + 1} ⟶ Y := ↾fun (x : PUnit.{u + 1}) ↦ y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x' = y
⊢ Eq (α := PUnit.{u + 1} → X) (fun (x : PUnit.{u + 1}) ↦ x')
    (⇑(hom (FC := TypeCat.Fun) (↑(Fork.IsLimit.lift' t y' hy') : PUnit.{u + 1} ⟶ (Fork.ofι f w).pt)) :
      (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (Fork.ofι f w).pt)
have a : Eq (α := PUnit.{u + 1} ⟶ X)
  ((Equiv.symm TypeCat.homEquiv : (a : PUnit.{u + 1} → X) → PUnit.{u + 1} ⟶ X) fun (x : PUnit.{u + 1}) ↦ x' :
    PUnit.{u + 1} ⟶ X)
  ((Equiv.symm TypeCat.homEquiv : (a : PUnit.{u + 1} → X) → PUnit.{u + 1} ⟶ X)
      (⇑(hom (FC := TypeCat.Fun) (↑(Fork.IsLimit.lift' t y' hy') : PUnit.{u + 1} ⟶ (Fork.ofι f w).pt)) :
        (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (Fork.ofι f w).pt) :
    PUnit.{u + 1} ⟶ X)
Tactic: apply TypeCat.homEquiv.symm.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy :
  Eq (α := (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
y' : PUnit.{u + 1} ⟶ Y := ↾fun (x : PUnit.{u + 1}) ↦ y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x' = y
⊢ Eq (α := PUnit.{u + 1} ⟶ X)
    ((Equiv.symm TypeCat.homEquiv : (a : PUnit.{u + 1} → X) → PUnit.{u + 1} ⟶ X) fun (x : PUnit.{u + 1}) ↦ x' :
      PUnit.{u + 1} ⟶ X)
    ((Equiv.symm TypeCat.homEquiv : (a : PUnit.{u + 1} → X) → PUnit.{u + 1} ⟶ X)
        (⇑(hom (FC := TypeCat.Fun) (↑(Fork.IsLimit.lift' t y' hy') : PUnit.{u + 1} ⟶ (Fork.ofι f w).pt)) :
          (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (Fork.ofι f w).pt) :
      PUnit.{u + 1} ⟶ X)
have a : Eq (α := PUnit.{u + 1} ⟶ Y)
  (((Equiv.symm TypeCat.homEquiv : (a : PUnit.{u + 1} → X) → PUnit.{u + 1} ⟶ X) fun (x : PUnit.{u + 1}) ↦ x') ≫
    (Fork.ofι f w).ι)
  ((Equiv.symm TypeCat.homEquiv : (a : PUnit.{u + 1} → X) → PUnit.{u + 1} ⟶ X)
      (⇑(hom (FC := TypeCat.Fun) (↑(Fork.IsLimit.lift' t y' hy') : PUnit.{u + 1} ⟶ (Fork.ofι f w).pt)) :
        (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (Fork.ofι f w).pt) ≫
    (Fork.ofι f w).ι)
Tactic: apply Fork.IsLimit.hom_ext t
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy :
  Eq (α := (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) y :
      (fun (X : Type u) ↦ X) Z)
y' : PUnit.{u + 1} ⟶ Y := ↾fun (x : PUnit.{u + 1}) ↦ y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x' = y
⊢ Eq (α := PUnit.{u + 1} ⟶ Y)
    (((Equiv.symm TypeCat.homEquiv : (a : PUnit.{u + 1} → X) → PUnit.{u + 1} ⟶ X) fun (x : PUnit.{u + 1}) ↦ x') ≫
      (Fork.ofι f w).ι)
    ((Equiv.symm TypeCat.homEquiv : (a : PUnit.{u + 1} → X) → PUnit.{u + 1} ⟶ X)
        (⇑(hom (FC := TypeCat.Fun) (↑(Fork.IsLimit.lift' t y' hy') : PUnit.{u + 1} ⟶ (Fork.ofι f w).pt)) :
          (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (Fork.ofι f w).pt) ≫
      (Fork.ofι f w).ι)
have a : TypeCat.Fun.toFun
    (hom (FC := TypeCat.Fun)
      (((Equiv.symm TypeCat.homEquiv : (a : PUnit.{u + 1} → X) → PUnit.{u + 1} ⟶ X) fun (x : PUnit.{u + 1}) ↦ x') ≫
        (Fork.ofι f w).ι))
    PUnit.unit =
  TypeCat.Fun.toFun
    (hom (FC := TypeCat.Fun)
      ((Equiv.symm TypeCat.homEquiv : (a : PUnit.{u + 1} → X) → PUnit.{u + 1} ⟶ X)
          (⇑(hom (FC := TypeCat.Fun) (↑(Fork.IsLimit.lift' t y' hy') : PUnit.{u + 1} ⟶ (Fork.ofι f w).pt)) :
            (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (Fork.ofι f w).pt) ≫
        (Fork.ofι f w).ι))
    PUnit.unit
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Equalizers (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
⊢ Eq (α :=
    { x : Y //
        Eq (α := (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
            (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
            (fun (X : Type u) ↦ X) Z) } ⟶
      Z)
    (↾Subtype.val (p := fun (x : Y) ↦
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
              (fun (X : Type u) ↦ X) Z)) ≫
      g)
    (↾Subtype.val (p := fun (x : Y) ↦
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
              (fun (X : Type u) ↦ X) Z)) ≫
      h)
have h₁ : ∀
  (x :
    { x : Y //
      Eq (α := (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
          (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
          (fun (X : Type u) ↦ X) Z) }),
  TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (↾Subtype.val (p := fun (x : Y) ↦
              Eq (α := (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)) ≫
          g))
      x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (↾Subtype.val (p := fun (x : Y) ↦
              Eq (α := (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)) ≫
          h))
      x
Tactic: ext x