-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X : PartialFun
h :
  (↑(ConcreteCategory.hom (FC := fun (X Y : Pointed.{u}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X)
            (X := partialFunToPointed.obj X) (Y := partialFunToPointed.obj X)
            (CategoryStruct.comp (Y := partialFunToPointed.obj (pointedToPartialFun.obj (partialFunToPointed.obj X)))
                (partialFunToPointed.map
                  (NatTrans.app
                    (Iso.hom
                      (NatIso.ofComponents
                        (fun (X : PartialFun.{u}) ↦
                          PartialFun.Iso.mk
                            {
                              toFun := fun (a : Functor.obj (𝟭 PartialFun) X) ↦
                                Subtype.mk (p := fun (x : (partialFunToPointed.obj X).X) ↦
                                  x ≠ (partialFunToPointed.obj X).point) (some a) ⋯,
                              invFun := fun (a : (partialFunToPointed ⋙ pointedToPartialFun).obj X) ↦
                                Option.get (↑a : (partialFunToPointed.obj X).X) ⋯,
                              left_inv := ⋯, right_inv := ⋯ })
                        ⋯))
                    X))
                (NatTrans.app
                  (Iso.hom
                    (NatIso.ofComponents (fun (X : Pointed.{u}) ↦ Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯) ⋯))
                  (partialFunToPointed.obj X)) :
              partialFunToPointed.obj X ⟶ partialFunToPointed.obj X)) :
        (partialFunToPointed.obj X).X → (partialFunToPointed.obj X).X)
      none =
    (↑(ConcreteCategory.hom (FC := fun (X Y : Pointed.{u}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X)
            (𝟙 (partialFunToPointed.obj X))) :
        (partialFunToPointed.obj X).X → (partialFunToPointed.obj X).X)
      none
h₁ :
  ∀ (x : X),
    (↑(ConcreteCategory.hom (FC := fun (X Y : Pointed.{u}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X)
              (X := partialFunToPointed.obj X) (Y := partialFunToPointed.obj X)
              (CategoryStruct.comp (Y := partialFunToPointed.obj (pointedToPartialFun.obj (partialFunToPointed.obj X)))
                  (partialFunToPointed.map
                    (NatTrans.app
                      (Iso.hom
                        (NatIso.ofComponents
                          (fun (X : PartialFun.{u}) ↦
                            PartialFun.Iso.mk
                              {
                                toFun := fun (a : Functor.obj (𝟭 PartialFun) X) ↦
                                  Subtype.mk (p := fun (x : (partialFunToPointed.obj X).X) ↦
                                    x ≠ (partialFunToPointed.obj X).point) (some a) ⋯,
                                invFun := fun (a : (partialFunToPointed ⋙ pointedToPartialFun).obj X) ↦
                                  Option.get (↑a : (partialFunToPointed.obj X).X) ⋯,
                                left_inv := ⋯, right_inv := ⋯ })
                          ⋯))
                      X))
                  (NatTrans.app
                    (Iso.hom
                      (NatIso.ofComponents (fun (X : Pointed.{u}) ↦ Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯)
                        ⋯))
                    (partialFunToPointed.obj X)) :
                partialFunToPointed.obj X ⟶ partialFunToPointed.obj X)) :
          (partialFunToPointed.obj X).X → (partialFunToPointed.obj X).X)
        (some x) =
      (↑(ConcreteCategory.hom (FC := fun (X Y : Pointed.{u}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
              Pointed.X) (𝟙 (partialFunToPointed.obj X))) :
          (partialFunToPointed.obj X).X → (partialFunToPointed.obj X).X)
        (some x)
⊢ Eq (α := partialFunToPointed.obj X ⟶ partialFunToPointed.obj X)
    (CategoryStruct.comp (Y := partialFunToPointed.obj (pointedToPartialFun.obj (partialFunToPointed.obj X)))
        (partialFunToPointed.map
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (X : PartialFun.{u}) ↦
                  PartialFun.Iso.mk
                    {
                      toFun := fun (a : Functor.obj (𝟭 PartialFun) X) ↦
                        Subtype.mk (p := fun (x : (partialFunToPointed.obj X).X) ↦
                          x ≠ (partialFunToPointed.obj X).point) (some a) ⋯,
                      invFun := fun (a : (partialFunToPointed ⋙ pointedToPartialFun).obj X) ↦
                        Option.get (↑a : (partialFunToPointed.obj X).X) ⋯,
                      left_inv := ⋯, right_inv := ⋯ })
                ⋯))
            X))
        (NatTrans.app
          (Iso.hom (NatIso.ofComponents (fun (X : Pointed.{u}) ↦ Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯) ⋯))
          (partialFunToPointed.obj X)) :
      partialFunToPointed.obj X ⟶ partialFunToPointed.obj X)
    (𝟙 (partialFunToPointed.obj X) : partialFunToPointed.obj X ⟶ partialFunToPointed.obj X)

Tactic:
ext (_ | x)