-- 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) ⋙
        bipointedToPointedFst)
      Y
h :
  Eq (α := Y.toBipointed.X)
    ((↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
              (InducedCategory.Hom.hom
                (({
                        toFun := fun (f : pointedToTwoPFst.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) ⋙
                                  bipointedToPointedFst)
                                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) ⋙
                                    bipointedToPointedFst)
                                  Y) ↦
                          {
                            hom :=
                              {
                                toFun := fun (o : (pointedToTwoPFst.obj X').toBipointed.X) ↦
                                  Option.elim o Y.toTwoPointing.toProd.2 f.toFun,
                                map_fst := ⋯, map_snd := ⋯ : (pointedToTwoPFst.obj X').toBipointed.Hom Y.toBipointed } :
                            InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPFst.obj X') Y },
                        left_inv := ⋯, right_inv := ⋯ :
                        (pointedToTwoPFst.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) ⋙
                                bipointedToPointedFst)
                              Y) }.symm :
                    (a : X' ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y) → pointedToTwoPFst.obj X' ⟶ Y)
                  (f ≫ g)))) :
          (pointedToTwoPFst.obj X').toBipointed.X → Y.toBipointed.X)
        none :
      Y.toBipointed.X)
    ((↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
              (InducedCategory.Hom.hom
                (pointedToTwoPFst.map f ≫
                  ({
                          toFun := fun (f : pointedToTwoPFst.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) ⋙
                                    bipointedToPointedFst)
                                  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) ⋙
                                      bipointedToPointedFst)
                                    Y) ↦
                            {
                              hom :=
                                {
                                  toFun := fun (o : (pointedToTwoPFst.obj X).toBipointed.X) ↦
                                    Option.elim o Y.toTwoPointing.toProd.2 f.toFun,
                                  map_fst := ⋯, map_snd := ⋯ :
                                  (pointedToTwoPFst.obj X).toBipointed.Hom Y.toBipointed } :
                              InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPFst.obj X) Y },
                          left_inv := ⋯, right_inv := ⋯ :
                          (pointedToTwoPFst.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) ⋙
                                  bipointedToPointedFst)
                                Y) }.symm :
                      (a : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y) → pointedToTwoPFst.obj X ⟶ Y)
                    g))) :
          (pointedToTwoPFst.obj X').toBipointed.X → Y.toBipointed.X)
        none :
      Y.toBipointed.X)
⊢ Eq (α := pointedToTwoPFst.obj X' ⟶ Y)
    (({
              toFun := fun (f : pointedToTwoPFst.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) ⋙
                        bipointedToPointedFst)
                      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) ⋙
                          bipointedToPointedFst)
                        Y) ↦
                {
                  hom :=
                    {
                      toFun := fun (o : (pointedToTwoPFst.obj X').toBipointed.X) ↦
                        Option.elim o Y.toTwoPointing.toProd.2 f.toFun,
                      map_fst := ⋯, map_snd := ⋯ : (pointedToTwoPFst.obj X').toBipointed.Hom Y.toBipointed } :
                  InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPFst.obj X') Y },
              left_inv := ⋯, right_inv := ⋯ :
              (pointedToTwoPFst.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) ⋙
                      bipointedToPointedFst)
                    Y) }.symm :
          (a : X' ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y) → pointedToTwoPFst.obj X' ⟶ Y)
        (f ≫ g) :
      pointedToTwoPFst.obj X' ⟶ Y)
    (pointedToTwoPFst.map f ≫
        ({
                toFun := fun (f : pointedToTwoPFst.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) ⋙
                          bipointedToPointedFst)
                        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) ⋙
                            bipointedToPointedFst)
                          Y) ↦
                  {
                    hom :=
                      {
                        toFun := fun (o : (pointedToTwoPFst.obj X).toBipointed.X) ↦
                          Option.elim o Y.toTwoPointing.toProd.2 f.toFun,
                        map_fst := ⋯, map_snd := ⋯ : (pointedToTwoPFst.obj X).toBipointed.Hom Y.toBipointed } :
                    InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPFst.obj X) Y },
                left_inv := ⋯, right_inv := ⋯ :
                (pointedToTwoPFst.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) ⋙
                        bipointedToPointedFst)
                      Y) }.symm :
            (a : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y) → pointedToTwoPFst.obj X ⟶ Y)
          g :
      pointedToTwoPFst.obj X' ⟶ Y)
have h₁ : ∀ (val : X'.X),
  Eq (α := Y.toBipointed.X)
    ((↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
              (InducedCategory.Hom.hom
                (({
                        toFun := fun (f : pointedToTwoPFst.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) ⋙
                                  bipointedToPointedFst)
                                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) ⋙
                                    bipointedToPointedFst)
                                  Y) ↦
                          {
                            hom :=
                              {
                                toFun := fun (o : (pointedToTwoPFst.obj X').toBipointed.X) ↦
                                  Option.elim o Y.toTwoPointing.toProd.2 f.toFun,
                                map_fst := sorry, map_snd := sorry : (pointedToTwoPFst.obj X').toBipointed.Hom Y.toBipointed } :
                            InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPFst.obj X') Y },
                        left_inv := sorry, right_inv := sorry :
                        (pointedToTwoPFst.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) ⋙
                                bipointedToPointedFst)
                              Y) }.symm :
                    (a : X' ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y) → pointedToTwoPFst.obj X' ⟶ Y)
                  (f ≫ g)))) :
          (pointedToTwoPFst.obj X').toBipointed.X → Y.toBipointed.X)
        (some val) :
      Y.toBipointed.X)
    ((↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
              (InducedCategory.Hom.hom
                (pointedToTwoPFst.map f ≫
                  ({
                          toFun := fun (f : pointedToTwoPFst.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) ⋙
                                    bipointedToPointedFst)
                                  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) ⋙
                                      bipointedToPointedFst)
                                    Y) ↦
                            {
                              hom :=
                                {
                                  toFun := fun (o : (pointedToTwoPFst.obj X).toBipointed.X) ↦
                                    Option.elim o Y.toTwoPointing.toProd.2 f.toFun,
                                  map_fst := sorry, map_snd := sorry :
                                  (pointedToTwoPFst.obj X).toBipointed.Hom Y.toBipointed } :
                              InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPFst.obj X) Y },
                          left_inv := sorry, right_inv := sorry :
                          (pointedToTwoPFst.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) ⋙
                                  bipointedToPointedFst)
                                Y) }.symm :
                      (a : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y) → pointedToTwoPFst.obj X ⟶ Y)
                    g))) :
          (pointedToTwoPFst.obj X').toBipointed.X → Y.toBipointed.X)
        (some val) :
      Y.toBipointed.X)
Tactic: ext (_ | _) : 4