-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X' X : Pointed
Y : Bipointed
f : X' ⟶ X
g : X ⟶ bipointedToPointedSnd.obj Y
x : (pointedToBipointedSnd.obj X').X
toFun :
  Eq (α := Y.X)
    (Bipointed.Hom.toFun (X := pointedToBipointedSnd.obj X')
      (({
              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))
      none)
    (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)
      none)
toFun₁ :
  ∀ (val : X'.X),
    Eq (α := Y.X)
      (Bipointed.Hom.toFun (X := pointedToBipointedSnd.obj X')
        (({
                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))
        (some val))
      (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)
        (some val))
⊢ 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)

Tactic:
cases x