awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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
⊢ 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)
              ⋯) ≫
          (Fork.ofι f w).ι))
      i =
    (hom (FC := TypeCat.Fun) s.ι).toFun i

Tactic:
(Classical.choose_spec (t (s.ι i) (congr_hom s.condition i))).1

Premises used: CategoryTheory.ConcreteCategory.hom, Classical.choose_spec, And.left, CategoryTheory.Limits.Fork.ι, Classical.choose, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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
⊢ 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)
              ⋯) ≫
          (Fork.ofι f w).ι))
      i =
    (hom (FC := TypeCat.Fun) s.ι).toFun i

Tactic:
exact (Classical.choose_spec (t (s.ι i) (congr_hom s.condition i))).1

Premises used: CategoryTheory.ConcreteCategory.hom, Classical.choose_spec, And.left, CategoryTheory.Limits.Fork.ι, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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.ι
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)
              ⋯))
        i
⊢ 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)
        ⋯

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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.ι
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)
            ⋯))
      i

Tactic:
(Classical.choose_spec (t (s.ι i) (congr_hom s.condition i))).2 _ (congr_hom hm i)

Premises used: CategoryTheory.ConcreteCategory.hom, Classical.choose_spec, And.right, CategoryTheory.Limits.Fork.ι, Classical.choose, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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.ι
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)
            ⋯))
      i

Tactic:
exact (Classical.choose_spec (t (s.ι i) (congr_hom s.condition i))).2 _ (congr_hom hm i)

Premises used: CategoryTheory.ConcreteCategory.hom, Classical.choose_spec, And.right, CategoryTheory.Limits.Fork.ι, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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
h₁ : ∀ (x : PUnit.{u + 1}), (hom (FC := TypeCat.Fun) (y' ≫ g)).toFun x = (hom (FC := TypeCat.Fun) (y' ≫ h)).toFun x
⊢ y' ≫ g = y' ≫ h

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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 : PUnit.{u + 1}
⊢ (hom (FC := TypeCat.Fun) (y' ≫ g)).toFun x = (hom (FC := TypeCat.Fun) (y' ≫ h)).toFun x

Tactic:
hy
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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 : PUnit.{u + 1}
⊢ (hom (FC := TypeCat.Fun) (y' ≫ g)).toFun x = (hom (FC := TypeCat.Fun) (y' ≫ h)).toFun x

Tactic:
exact hy
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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

Tactic:
have hy' : y' ≫ g = y' ≫ h := by ext; exact hy
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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

Tactic:
⟨(Fork.IsLimit.lift' t _ hy').1 ⟨⟩, congr_hom (Fork.IsLimit.lift' t y' _).2 ⟨⟩, ?_⟩

Premises used: CategoryTheory.Limits.Fork.IsLimit.lift', CategoryTheory.ConcreteCategory.hom, ExistsUnique, And.intro, Exists.intro, PUnit.unit, Subtype.val, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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
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
⊢ ∃! x : X, (hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x = y

Tactic:
refine ⟨(Fork.IsLimit.lift' t _ hy').1 ⟨⟩, congr_hom (Fork.IsLimit.lift' t y' _).2 ⟨⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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)
rw rw₁ : x' = (fun (x : PUnit.{u + 1}) ↦ x') PUnit.unit
⊢ 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

Tactic:
rw [← this]
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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
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)
⊢ 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

Tactic:
suffices (fun _ : PUnit => x') = (Fork.IsLimit.lift' t y' hy').1 by
    rw [← this]
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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
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)
⊢ 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:
apply TypeCat.homEquiv.symm.injective

Premises used: TypeCat.homEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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
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).ι)
⊢ 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 Fork.IsLimit.hom_ext t

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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
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
⊢ 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:
ext ⟨⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
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
⊢ 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:
apply hx'.trans (congr_hom (Fork.IsLimit.lift' t _ hy').2 ⟨⟩).symm

Premises used: CategoryTheory.Limits.Fork.IsLimit.lift', CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, Eq.trans, Subtype.property