-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
h :
  (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
            (InducedCategory.Hom.hom
              ((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))
                ((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) })
                  f)))) :
        (pointedToTwoPFst.obj X).toBipointed.X → Y.toBipointed.X)
      none =
    (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X) f.hom) :
        (pointedToTwoPFst.obj X).toBipointed.X → Y.toBipointed.X)
      none
h₁ :
  ∀ (val : X.X),
    (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
              (InducedCategory.Hom.hom
                ((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))
                  ((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) })
                    f)))) :
          (pointedToTwoPFst.obj X).toBipointed.X → Y.toBipointed.X)
        (some val) =
      (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X) f.hom) :
          (pointedToTwoPFst.obj X).toBipointed.X → Y.toBipointed.X)
        (some val)
⊢ (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 := ⋯ } } :
          InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPFst.obj X) Y))
      ((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) })
        f) =
    f

Tactic:
ext (_ | _) : 4