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