-- Lean 4 proof step from Mathlib.CategoryTheory.Category.TwoP (goal)
Goal:
α : Type u_1
β : Type u_2
X' X : Pointed
Y : TwoP
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
          fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD := Bipointed.X) ⋙
        bipointedToPointedSnd)
      Y
⊢ Eq (α := pointedToTwoPSnd.obj X' ⟶ Y)
    (({
              toFun := fun (f : pointedToTwoPSnd.obj X' ⟶ Y) ↦
                { toFun := f.hom.toFun ∘ some, map_point := ⋯ :
                  X'.Hom
                    (Functor.obj
                      (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                          fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                          Bipointed.X) ⋙
                        bipointedToPointedSnd)
                      Y) },
              invFun :=
                fun
                  (f :
                    X' ⟶
                      Functor.obj
                        (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                            fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                            Bipointed.X) ⋙
                          bipointedToPointedSnd)
                        Y) ↦
                {
                  hom :=
                    {
                      toFun := fun (o : (pointedToTwoPSnd.obj X').toBipointed.X) ↦
                        Option.elim o Y.toTwoPointing.toProd.1 f.toFun,
                      map_fst := ⋯, map_snd := ⋯ : (pointedToTwoPSnd.obj X').toBipointed.Hom Y.toBipointed } :
                  InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPSnd.obj X') Y },
              left_inv := ⋯, right_inv := ⋯ :
              (pointedToTwoPSnd.obj X' ⟶ Y) ≃
                (X' ⟶
                  Functor.obj
                    (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                        fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                        Bipointed.X) ⋙
                      bipointedToPointedSnd)
                    Y) }.symm :
          (a : X' ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y) → pointedToTwoPSnd.obj X' ⟶ Y)
        (f ≫ g) :
      pointedToTwoPSnd.obj X' ⟶ Y)
    (pointedToTwoPSnd.map f ≫
        ({
                toFun := fun (f : pointedToTwoPSnd.obj X ⟶ Y) ↦
                  { toFun := f.hom.toFun ∘ some, map_point := ⋯ :
                    X.Hom
                      (Functor.obj
                        (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                            fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                            Bipointed.X) ⋙
                          bipointedToPointedSnd)
                        Y) },
                invFun :=
                  fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedSnd)
                          Y) ↦
                  {
                    hom :=
                      {
                        toFun := fun (o : (pointedToTwoPSnd.obj X).toBipointed.X) ↦
                          Option.elim o Y.toTwoPointing.toProd.1 f.toFun,
                        map_fst := ⋯, map_snd := ⋯ : (pointedToTwoPSnd.obj X).toBipointed.Hom Y.toBipointed } :
                    InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPSnd.obj X) Y },
                left_inv := ⋯, right_inv := ⋯ :
                (pointedToTwoPSnd.obj X ⟶ Y) ≃
                  (X ⟶
                    Functor.obj
                      (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                          fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                          Bipointed.X) ⋙
                        bipointedToPointedSnd)
                      Y) }.symm :
            (a : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y) → pointedToTwoPSnd.obj X ⟶ Y)
          g :
      pointedToTwoPSnd.obj X' ⟶ Y)
have h : Eq (α := Y.toBipointed.X)
  ((↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
            (InducedCategory.Hom.hom
              (({
                      toFun := fun (f : pointedToTwoPSnd.obj X' ⟶ Y) ↦
                        { toFun := f.hom.toFun ∘ some, map_point := sorry :
                          X'.Hom
                            (Functor.obj
                              (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed)
                                  (CC := fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype)
                                  (CD := Bipointed.X) ⋙
                                bipointedToPointedSnd)
                              Y) },
                      invFun :=
                        fun
                          (f :
                            X' ⟶
                              Functor.obj
                                (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed)
                                    (CC := fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD :=
                                    Bipointed.HomSubtype) (CD := Bipointed.X) ⋙
                                  bipointedToPointedSnd)
                                Y) ↦
                        {
                          hom :=
                            {
                              toFun := fun (o : (pointedToTwoPSnd.obj X').toBipointed.X) ↦
                                Option.elim o Y.toTwoPointing.toProd.1 f.toFun,
                              map_fst := sorry, map_snd := sorry : (pointedToTwoPSnd.obj X').toBipointed.Hom Y.toBipointed } :
                          InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPSnd.obj X') Y },
                      left_inv := sorry, right_inv := sorry :
                      (pointedToTwoPSnd.obj X' ⟶ Y) ≃
                        (X' ⟶
                          Functor.obj
                            (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                                fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                                Bipointed.X) ⋙
                              bipointedToPointedSnd)
                            Y) }.symm :
                  (a : X' ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y) → pointedToTwoPSnd.obj X' ⟶ Y)
                (f ≫ g)))) :
        (pointedToTwoPSnd.obj X').toBipointed.X → Y.toBipointed.X)
      none :
    Y.toBipointed.X)
  ((↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
            (InducedCategory.Hom.hom
              (pointedToTwoPSnd.map f ≫
                ({
                        toFun := fun (f : pointedToTwoPSnd.obj X ⟶ Y) ↦
                          { toFun := f.hom.toFun ∘ some, map_point := sorry :
                            X.Hom
                              (Functor.obj
                                (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed)
                                    (CC := fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD :=
                                    Bipointed.HomSubtype) (CD := Bipointed.X) ⋙
                                  bipointedToPointedSnd)
                                Y) },
                        invFun :=
                          fun
                            (f :
                              X ⟶
                                Functor.obj
                                  (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed)
                                      (CC := fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD :=
                                      Bipointed.HomSubtype) (CD := Bipointed.X) ⋙
                                    bipointedToPointedSnd)
                                  Y) ↦
                          {
                            hom :=
                              {
                                toFun := fun (o : (pointedToTwoPSnd.obj X).toBipointed.X) ↦
                                  Option.elim o Y.toTwoPointing.toProd.1 f.toFun,
                                map_fst := sorry, map_snd := sorry : (pointedToTwoPSnd.obj X).toBipointed.Hom Y.toBipointed } :
                            InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPSnd.obj X) Y },
                        left_inv := sorry, right_inv := sorry :
                        (pointedToTwoPSnd.obj X ⟶ Y) ≃
                          (X ⟶
                            Functor.obj
                              (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed)
                                  (CC := fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype)
                                  (CD := Bipointed.X) ⋙
                                bipointedToPointedSnd)
                              Y) }.symm :
                    (a : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y) → pointedToTwoPSnd.obj X ⟶ Y)
                  g))) :
        (pointedToTwoPSnd.obj X').toBipointed.X → Y.toBipointed.X)
      none :
    Y.toBipointed.X)
Tactic: ext (_ | _) : 4