-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Bipointed (goal)
Goal:
X' X : Pointed
Y : Bipointed
f : X' ⟶ X
g : X ⟶ bipointedToPointedSnd.obj Y
x : (pointedToBipointedSnd.obj X').X
⊢ Eq (α := 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))
      x)
    (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)
      x)
have toFun : Eq (α := Y.X)
  (Bipointed.Hom.toFun (X := pointedToBipointedSnd.obj X')
    (({
            toFun := fun (f : pointedToBipointedSnd.obj X' ⟶ Y) ↦
              { toFun := f.toFun ∘ some, map_point := sorry : 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 := sorry,
                map_snd := sorry : (pointedToBipointedSnd.obj X').Hom Y },
            left_inv := sorry, right_inv := sorry :
            (pointedToBipointedSnd.obj X' ⟶ Y) ≃ (X' ⟶ bipointedToPointedSnd.obj Y) }.symm :
        (a : X' ⟶ bipointedToPointedSnd.obj Y) → pointedToBipointedSnd.obj X' ⟶ Y)
      (f ≫ g))
    none)
  (Bipointed.Hom.toFun
    (pointedToBipointedSnd.map f ≫
      ({
              toFun := fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
                { toFun := f.toFun ∘ some, map_point := sorry : 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 := sorry,
                  map_snd := sorry : (pointedToBipointedSnd.obj X).Hom Y },
              left_inv := sorry, right_inv := sorry :
              (pointedToBipointedSnd.obj X ⟶ Y) ≃ (X ⟶ bipointedToPointedSnd.obj Y) }.symm :
          (a : X ⟶ bipointedToPointedSnd.obj Y) → pointedToBipointedSnd.obj X ⟶ Y)
        g)
    none)
Tactic: cases x
Cleared hypotheses: x