-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X' X : Pointed
Y : Bipointed
f : X' ⟶ X
g : X ⟶ bipointedToPointedSnd.obj Y
toFun :
  Eq (α := (pointedToBipointedSnd.obj X').X → Y.X)
    (Bipointed.Hom.toFun
      (({
              toFun := fun (f : pointedToBipointedSnd.obj X' ⟶ Y) ↦
                { toFun := f.toFun ∘ some, map_point := ⋯ : X'.Hom (bipointedToPointedSnd.obj Y) },
              invFun := fun (f : X' ⟶ bipointedToPointedSnd.obj Y) ↦
                { toFun := fun (o : (pointedToBipointedSnd.obj X').X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
                  map_snd := ⋯ : (pointedToBipointedSnd.obj X').Hom Y },
              left_inv := ⋯, right_inv := ⋯ :
              (pointedToBipointedSnd.obj X' ⟶ Y) ≃ (X' ⟶ bipointedToPointedSnd.obj Y) }.symm :
          (a : X' ⟶ bipointedToPointedSnd.obj Y) → pointedToBipointedSnd.obj X' ⟶ Y)
        (f ≫ g)))
    (Bipointed.Hom.toFun
      (pointedToBipointedSnd.map f ≫
        ({
                toFun := fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
                  { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) },
                invFun := fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
                  { toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
                    map_snd := ⋯ : (pointedToBipointedSnd.obj X).Hom Y },
                left_inv := ⋯, right_inv := ⋯ :
                (pointedToBipointedSnd.obj X ⟶ Y) ≃ (X ⟶ bipointedToPointedSnd.obj Y) }.symm :
            (a : X ⟶ bipointedToPointedSnd.obj Y) → pointedToBipointedSnd.obj X ⟶ Y)
          g))
⊢ Eq (α := pointedToBipointedSnd.obj X' ⟶ Y)
    (({
              toFun := fun (f : pointedToBipointedSnd.obj X' ⟶ Y) ↦
                { toFun := f.toFun ∘ some, map_point := ⋯ : X'.Hom (bipointedToPointedSnd.obj Y) },
              invFun := fun (f : X' ⟶ bipointedToPointedSnd.obj Y) ↦
                { toFun := fun (o : (pointedToBipointedSnd.obj X').X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
                  map_snd := ⋯ : (pointedToBipointedSnd.obj X').Hom Y },
              left_inv := ⋯, right_inv := ⋯ :
              (pointedToBipointedSnd.obj X' ⟶ Y) ≃ (X' ⟶ bipointedToPointedSnd.obj Y) }.symm :
          (a : X' ⟶ bipointedToPointedSnd.obj Y) → pointedToBipointedSnd.obj X' ⟶ Y)
        (f ≫ g) :
      pointedToBipointedSnd.obj X' ⟶ Y)
    (pointedToBipointedSnd.map f ≫
        ({
                toFun := fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
                  { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) },
                invFun := fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
                  { toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
                    map_snd := ⋯ : (pointedToBipointedSnd.obj X).Hom Y },
                left_inv := ⋯, right_inv := ⋯ :
                (pointedToBipointedSnd.obj X ⟶ Y) ≃ (X ⟶ bipointedToPointedSnd.obj Y) }.symm :
            (a : X ⟶ bipointedToPointedSnd.obj Y) → pointedToBipointedSnd.obj X ⟶ Y)
          g :
      pointedToBipointedSnd.obj X' ⟶ Y)

Tactic:
apply Bipointed.Hom.ext

Premises used: Bipointed.Hom.ext