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

Tactic:
apply Bipointed.Hom.ext

Premises used: Bipointed.Hom.ext