-- Lean 4 proof step from Mathlib.CategoryTheory.Category.TwoP (goal)
Goal:
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.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) ⋙
                            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))
                ((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) })
                  f)))) :
        (pointedToTwoPSnd.obj X).toBipointed.X → Y.toBipointed.X)
      none =
    (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X) f.hom) :
        (pointedToTwoPSnd.obj X).toBipointed.X → Y.toBipointed.X)
      none
⊢ (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 := ⋯ } } :
          InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPSnd.obj X) Y))
      ((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) })
        f) =
    f
have 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) ⋙
                            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))
                ((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) })
                  f)))) :
        (pointedToTwoPSnd.obj X).toBipointed.X → Y.toBipointed.X)
      (some val) =
    (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X) f.hom) :
        (pointedToTwoPSnd.obj X).toBipointed.X → Y.toBipointed.X)
      (some val)
Tactic: ext (_ | _) : 4