awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J_1 : Type u
inst : Category.{v, u} J_1
F_1 : J_1ᵒᵖ ⥤ J_1 ⥤ Type (max w u)
J : Type u
inst_1 : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
m : s.pt ⟶ (wedge.{w, v, u} F).pt
h : ∀ (j : WalkingMulticospan (multicospanShapeEnd.{v, u} J)), m ≫ (wedge.{w, v, u} F).π.app j = s.π.app j
x : s.pt
h₁ :
  (↑((hom (FC := Fun) m).toFun x) : (j : J) → (F.obj (op j)).obj j) =
    (↑(Fun.toFun
          (hom (FC := Fun)
            (↾fun (x : s.pt) ↦
              Subtype.mk (p := fun (x : (j : J) → (F.obj (op j)).obj j) ↦
                ∀ ⦃i j : J⦄ (f : i ⟶ j),
                  Eq (α := (F.obj (op i)).obj j)
                    ((Hom.hom ((F.obj (op i)).map f) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j) (x i) :
                      (F.obj (op i)).obj j)
                    ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j)).obj j) → (F.obj (op i)).obj j) (x j) :
                      (F.obj (op i)).obj j))
                (fun (j : J) ↦
                  (hom (FC := Fun) (Multifork.ι s j) :
                      (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                        (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
                    x)
                ⋯))
          x) :
      (j : J) → (F.obj (op j)).obj j)
⊢ (hom (FC := Fun) m).toFun x =
    Fun.toFun
      (hom (FC := Fun)
        (↾fun (x : s.pt) ↦
          Subtype.mk (p := fun (x : (j : J) → (F.obj (op j)).obj j) ↦
            ∀ ⦃i j : J⦄ (f : i ⟶ j),
              Eq (α := (F.obj (op i)).obj j)
                ((Hom.hom ((F.obj (op i)).map f) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j) (x i) :
                  (F.obj (op i)).obj j)
                ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j)).obj j) → (F.obj (op i)).obj j) (x j) :
                  (F.obj (op i)).obj j))
            (fun (j : J) ↦
              (hom (FC := Fun) (Multifork.ι s j) :
                  (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                    (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
                x)
            ⋯))
      x

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J_1 : Type u
inst : Category.{v, u} J_1
F_1 : J_1ᵒᵖ ⥤ J_1 ⥤ Type (max w u)
J : Type u
inst_1 : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
m : s.pt ⟶ (wedge.{w, v, u} F).pt
h : ∀ (j : WalkingMulticospan (multicospanShapeEnd.{v, u} J)), m ≫ (wedge.{w, v, u} F).π.app j = s.π.app j
x : s.pt
h₁ :
  ∀ (j : J),
    (↑((hom (FC := Fun) m).toFun x) : (j : J) → (F.obj (op j)).obj j) j =
      (↑(Fun.toFun
              (hom (FC := Fun)
                (↾fun (x : s.pt) ↦
                  Subtype.mk (p := fun (x : (j : J) → (F.obj (op j)).obj j) ↦
                    ∀ ⦃i j : J⦄ (f : i ⟶ j),
                      Eq (α := (F.obj (op i)).obj j)
                        ((Hom.hom ((F.obj (op i)).map f) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j) (x i) :
                          (F.obj (op i)).obj j)
                        ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j)).obj j) → (F.obj (op i)).obj j) (x j) :
                          (F.obj (op i)).obj j))
                    (fun (j : J) ↦
                      (hom (FC := Fun) (Multifork.ι s j) :
                          (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                            (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
                        x)
                    ⋯))
              x) :
          (j : J) → (F.obj (op j)).obj j)
        j
⊢ (↑((hom (FC := Fun) m).toFun x) : (j : J) → (F.obj (op j)).obj j) =
    (↑(Fun.toFun
          (hom (FC := Fun)
            (↾fun (x : s.pt) ↦
              Subtype.mk (p := fun (x : (j : J) → (F.obj (op j)).obj j) ↦
                ∀ ⦃i j : J⦄ (f : i ⟶ j),
                  Eq (α := (F.obj (op i)).obj j)
                    ((Hom.hom ((F.obj (op i)).map f) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j) (x i) :
                      (F.obj (op i)).obj j)
                    ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j)).obj j) → (F.obj (op i)).obj j) (x j) :
                      (F.obj (op i)).obj j))
                (fun (j : J) ↦
                  (hom (FC := Fun) (Multifork.ι s j) :
                      (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                        (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
                    x)
                ⋯))
          x) :
      (j : J) → (F.obj (op j)).obj j)

Tactic:
funext j
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J_1 : Type u
inst : Category.{v, u} J_1
F_1 : J_1ᵒᵖ ⥤ J_1 ⥤ Type (max w u)
J : Type u
inst_1 : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
m : s.pt ⟶ (wedge.{w, v, u} F).pt
h : ∀ (j : WalkingMulticospan (multicospanShapeEnd.{v, u} J)), m ≫ (wedge.{w, v, u} F).π.app j = s.π.app j
x : s.pt
j : J
⊢ (↑((hom (FC := Fun) m).toFun x) : (j : J) → (F.obj (op j)).obj j) j =
    (↑(Fun.toFun
            (hom (FC := Fun)
              (↾fun (x : s.pt) ↦
                Subtype.mk (p := fun (x : (j : J) → (F.obj (op j)).obj j) ↦
                  ∀ ⦃i j : J⦄ (f : i ⟶ j),
                    Eq (α := (F.obj (op i)).obj j)
                      ((Hom.hom ((F.obj (op i)).map f) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j) (x i) :
                        (F.obj (op i)).obj j)
                      ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j)).obj j) → (F.obj (op i)).obj j) (x j) :
                        (F.obj (op i)).obj j))
                  (fun (j : J) ↦
                    (hom (FC := Fun) (Multifork.ι s j) :
                        (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                          (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
                      x)
                  ⋯))
            x) :
        (j : J) → (F.obj (op j)).obj j)
      j

Tactic:
ConcreteCategory.congr_hom (h (.left j)) x

Premises used: CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.WalkingMulticospan.left
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J_1 : Type u
inst : Category.{v, u} J_1
F_1 : J_1ᵒᵖ ⥤ J_1 ⥤ Type (max w u)
J : Type u
inst_1 : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
m : s.pt ⟶ (wedge.{w, v, u} F).pt
h : ∀ (j : WalkingMulticospan (multicospanShapeEnd.{v, u} J)), m ≫ (wedge.{w, v, u} F).π.app j = s.π.app j
x : s.pt
j : J
⊢ (↑((hom (FC := Fun) m).toFun x) : (j : J) → (F.obj (op j)).obj j) j =
    (↑(Fun.toFun
            (hom (FC := Fun)
              (↾fun (x : s.pt) ↦
                Subtype.mk (p := fun (x : (j : J) → (F.obj (op j)).obj j) ↦
                  ∀ ⦃i j : J⦄ (f : i ⟶ j),
                    Eq (α := (F.obj (op i)).obj j)
                      ((Hom.hom ((F.obj (op i)).map f) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j) (x i) :
                        (F.obj (op i)).obj j)
                      ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j)).obj j) → (F.obj (op i)).obj j) (x j) :
                        (F.obj (op i)).obj j))
                  (fun (j : J) ↦
                    (hom (FC := Fun) (Multifork.ι s j) :
                        (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                          (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
                      x)
                  ⋯))
            x) :
        (j : J) → (F.obj (op j)).obj j)
      j

Tactic:
exact ConcreteCategory.congr_hom (h (.left j)) x

Premises used: CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.WalkingMulticospan.left
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
⊢ chosenEnd F = end_.{w, v, u} F

Tactic:
rfl

Premises used: CategoryTheory.Limits.chosenEnd, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j : J
x : Types.end_.{w, v, u} F
⊢ (hom (FC := Fun) (π F j) : (a : chosenEnd F) → (F.obj (op j)).obj j) x = (↑x : (j : J) → (F.obj (op j)).obj j) j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
X : Type (max w u)
f : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f i ≫ (F.obj (op i)).map g = f j ≫ (F.map g.op).app j
x : X
⊢ Eq (α := chosenEnd F) ((hom (FC := Fun) (lift f hf) : (a : X) → chosenEnd F) x : chosenEnd F)
    (Subtype.mk (p := fun (x : (j : J) → (F.obj (op j)).obj j) ↦
        ∀ ⦃i j : J⦄ (f : i ⟶ j),
          Eq (α := (F.obj (op i)).obj j)
            ((Hom.hom ((F.obj (op i)).map f) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j) (x i) :
              (F.obj (op i)).obj j)
            ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j)).obj j) → (F.obj (op i)).obj j) (x j) :
              (F.obj (op i)).obj j))
        (fun (j : J) ↦ (hom (FC := Fun) (f j) : (a : X) → (F.obj (op j)).obj j) x) ⋯ :
      { x : (j : J) → (F.obj (op j)).obj j //
        ∀ ⦃i j : J⦄ (f : i ⟶ j),
          Eq (α := (F.obj (op i)).obj j)
            ((Hom.hom ((F.obj (op i)).map f) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j) (x i) :
              (F.obj (op i)).obj j)
            ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j)).obj j) → (F.obj (op i)).obj j) (x j) :
              (F.obj (op i)).obj j) })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J_1 : Type u
inst : Category.{v, u} J_1
F_1 : J_1ᵒᵖ ⥤ J_1 ⥤ Type (max w u)
J : Type u
inst_1 : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : Types.end_.{w, v, u} F
i j : J
g : i ⟶ j
rw :
  Eq (α := (G.obj (op i)).obj j)
    ((hom (FC := Fun) (NatTrans.app (f.app (op i)) j) : (a : (F.obj (op i)).obj j) → (G.obj (op i)).obj j)
        ((hom (FC := Fun) ((F.obj (op i)).map g) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j)
          ((↑x : (j : J) → (F.obj (op j)).obj j) i)) :
      (G.obj (op i)).obj j)
    ((Hom.hom ((G.map g.op).app j) : (a : (G.obj (op j)).obj j) → (G.obj (op i)).obj j)
        ((fun (j : J) ↦
            ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
                  (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
                    (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
                ((↑x : (j : J) → (F.obj (op j)).obj j) j) :
              (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j)))
          j) :
      (G.obj (op i)).obj j)
⊢ Eq (α := (G.obj (op i)).obj j)
    ((Hom.hom ((G.obj (op i)).map g) : (a : (G.obj (op i)).obj i) → (G.obj (op i)).obj j)
      ((fun (j : J) ↦
          ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
                (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
                  (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
              ((↑x : (j : J) → (F.obj (op j)).obj j) j) :
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j)))
        i))
    ((Hom.hom ((G.map g.op).app j) : (a : (G.obj (op j)).obj j) → (G.obj (op i)).obj j)
      ((fun (j : J) ↦
          ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
                (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
                  (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
              ((↑x : (j : J) → (F.obj (op j)).obj j) j) :
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j)))
        j))

Tactic:
rw [← (f.app (op i)).naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply, Opposite.op, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J_1 : Type u
inst : Category.{v, u} J_1
F_1 : J_1ᵒᵖ ⥤ J_1 ⥤ Type (max w u)
J : Type u
inst_1 : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : Types.end_.{w, v, u} F
i j : J
g : i ⟶ j
⊢ Eq (α := (G.obj (op i)).obj j)
    ((hom (FC := Fun) (NatTrans.app (f.app (op i)) j) : (a : (F.obj (op i)).obj j) → (G.obj (op i)).obj j)
        ((hom (FC := Fun) ((F.obj (op i)).map g) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j)
          ((↑x : (j : J) → (F.obj (op j)).obj j) i)) :
      (G.obj (op i)).obj j)
    ((Hom.hom ((G.map g.op).app j) : (a : (G.obj (op j)).obj j) → (G.obj (op i)).obj j)
        ((fun (j : J) ↦
            ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
                  (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
                    (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
                ((↑x : (j : J) → (F.obj (op j)).obj j) j) :
              (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j)))
          j) :
      (G.obj (op i)).obj j)

Tactic:
simp [x.2 g, ← comp_apply, -types_comp_apply]

Premises used: CategoryTheory.comp_apply, Subtype.property, CategoryTheory.types_comp_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : Types.end_.{w, v, u} F
⊢ Eq (α := chosenEnd G) ((hom (FC := Fun) (map f) : (a : chosenEnd F) → chosenEnd G) x : chosenEnd G)
    (Subtype.mk (p := fun (x : (j : J) → (G.obj (op j)).obj j) ↦
        ∀ ⦃i j : J⦄ (f : i ⟶ j),
          Eq (α := (G.obj (op i)).obj j)
            ((Hom.hom ((G.obj (op i)).map f) : (a : (G.obj (op i)).obj i) → (G.obj (op i)).obj j) (x i) :
              (G.obj (op i)).obj j)
            ((Hom.hom ((G.map f.op).app j) : (a : (G.obj (op j)).obj j) → (G.obj (op i)).obj j) (x j) :
              (G.obj (op i)).obj j))
        (fun (j : J) ↦
          (hom (FC := Fun) (NatTrans.app (f.app (op j)) j) : (a : (F.obj (op j)).obj j) → (G.obj (op j)).obj j)
            ((↑x : (j : J) → (F.obj (op j)).obj j) j))
        ⋯ :
      { x : (j : J) → (G.obj (op j)).obj j //
        ∀ ⦃i j : J⦄ (f : i ⟶ j),
          Eq (α := (G.obj (op i)).obj j)
            ((Hom.hom ((G.obj (op i)).map f) : (a : (G.obj (op i)).obj i) → (G.obj (op i)).obj j) (x i) :
              (G.obj (op i)).obj j)
            ((Hom.hom ((G.map f.op).app j) : (a : (G.obj (op j)).obj j) → (G.obj (op i)).obj j) (x j) :
              (G.obj (op i)).obj j) })

Tactic:
rfl

Premises used: rfl
-- 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
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.ι
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)
            ⋯
⊢ { 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 }

Tactic:
refine ⟨↾fun 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
i : s.pt
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)
⊢ (Fork.ofι f w).pt

Tactic:
apply Classical.choose (t (s.ι i) _)

Premises used: CategoryTheory.ConcreteCategory.hom, 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
⊢ 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 congr_hom s.condition i

Premises used: CategoryTheory.Limits.Fork.condition, CategoryTheory.ConcreteCategory.congr_hom
-- 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
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)
                ⋯) ≫
            (Fork.ofι f w).ι))
        i =
      (hom (FC := TypeCat.Fun) s.ι).toFun i
⊢ (↾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.ι

Tactic:
ext i