-- Module: Mathlib.CategoryTheory.Category.TwoP
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 (α := 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 := ⋯ :
                            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').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 := ⋯ :
                              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').toBipointed.X → Y.toBipointed.X)
        none :
      Y.toBipointed.X)

Tactic:
rfl