-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
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
⊢ 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)
have 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) sorry,
                              invFun := fun (a : (partialFunToPointed ⋙ pointedToPartialFun).obj X) ↦
                                Option.get (↑a : (partialFunToPointed.obj X).X) sorry,
                              left_inv := sorry, right_inv := sorry })
                        sorry))
                    X))
                (NatTrans.app
                  (Iso.hom
                    (NatIso.ofComponents (fun (X : Pointed.{u}) ↦ Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) sorry) sorry))
                  (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)
Tactic: ext (_ | x)