-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
α : Type u_1
β : Type u_2
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
h :
  Eq (α :=
    { X := Option X.X,
            toTwoPointing :=
              { fst := none, snd := some X.point, fst_ne_snd := ⋯ : TwoPointing (Option X.X) } }.toBipointed.X →
      { X := Option Z.X,
            toTwoPointing :=
              { fst := none, snd := some Z.point, fst_ne_snd := ⋯ : TwoPointing (Option Z.X) } }.toBipointed.X)
    (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
          (InducedCategory.Hom.hom
            {
              hom :=
                { toFun := Option.map (f ≫ g).toFun, map_fst := ⋯, map_snd := ⋯ :
                  { X := Option X.X,
                          toTwoPointing :=
                            { fst := none, snd := some X.point, fst_ne_snd := ⋯ : TwoPointing (Option X.X) } :
                          TwoP.{u} }.toBipointed.Hom
                    { X := Option Z.X,
                        toTwoPointing :=
                          { fst := none, snd := some Z.point, fst_ne_snd := ⋯ : TwoPointing (Option Z.X) } :
                        TwoP.{u} }.toBipointed } :
              InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed)
                { X := Option X.X,
                  toTwoPointing := { fst := none, snd := some X.point, fst_ne_snd := ⋯ : TwoPointing (Option X.X) } :
                  TwoP.{u} }
                { X := Option Z.X,
                  toTwoPointing := { fst := none, snd := some Z.point, fst_ne_snd := ⋯ : TwoPointing (Option Z.X) } :
                  TwoP.{u} } })) :
      { X := Option X.X, toTwoPointing := { fst := none, snd := some X.point, fst_ne_snd := ⋯ } }.toBipointed.X →
        { X := Option Z.X, toTwoPointing := { fst := none, snd := some Z.point, fst_ne_snd := ⋯ } }.toBipointed.X)
    (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
          (InducedCategory.Hom.hom
            (CategoryStruct.comp (Y :=
              { X := Option Y.X,
                toTwoPointing := { fst := none, snd := some Y.point, fst_ne_snd := ⋯ : TwoPointing (Option Y.X) } :
                TwoP.{u} })
              {
                hom :=
                  { toFun := Option.map f.toFun, map_fst := ⋯, map_snd := ⋯ :
                    { X := Option X.X,
                            toTwoPointing :=
                              { fst := none, snd := some X.point, fst_ne_snd := ⋯ : TwoPointing (Option X.X) } :
                            TwoP.{u} }.toBipointed.Hom
                      { X := Option Y.X,
                          toTwoPointing :=
                            { fst := none, snd := some Y.point, fst_ne_snd := ⋯ : TwoPointing (Option Y.X) } :
                          TwoP.{u} }.toBipointed } :
                InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed)
                  { X := Option X.X,
                    toTwoPointing := { fst := none, snd := some X.point, fst_ne_snd := ⋯ : TwoPointing (Option X.X) } :
                    TwoP.{u} }
                  { X := Option Y.X,
                    toTwoPointing := { fst := none, snd := some Y.point, fst_ne_snd := ⋯ : TwoPointing (Option Y.X) } :
                    TwoP.{u} } }
              {
                hom :=
                  { toFun := Option.map g.toFun, map_fst := ⋯, map_snd := ⋯ :
                    { X := Option Y.X,
                            toTwoPointing :=
                              { fst := none, snd := some Y.point, fst_ne_snd := ⋯ : TwoPointing (Option Y.X) } :
                            TwoP.{u} }.toBipointed.Hom
                      { X := Option Z.X,
                          toTwoPointing :=
                            { fst := none, snd := some Z.point, fst_ne_snd := ⋯ : TwoPointing (Option Z.X) } :
                          TwoP.{u} }.toBipointed } :
                InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed)
                  { X := Option Y.X,
                    toTwoPointing := { fst := none, snd := some Y.point, fst_ne_snd := ⋯ : TwoPointing (Option Y.X) } :
                    TwoP.{u} }
                  { X := Option Z.X,
                    toTwoPointing := { fst := none, snd := some Z.point, fst_ne_snd := ⋯ : TwoPointing (Option Z.X) } :
                    TwoP.{u} } }))) :
      { X := Option X.X, toTwoPointing := { fst := none, snd := some X.point, fst_ne_snd := ⋯ } }.toBipointed.X →
        { X := Option Z.X, toTwoPointing := { fst := none, snd := some Z.point, fst_ne_snd := ⋯ } }.toBipointed.X)
⊢ Eq.{u + 1} (α :=
    { X := Option X.X,
        toTwoPointing := { fst := none, snd := some X.point, fst_ne_snd := ⋯ : TwoPointing (Option X.X) } : TwoP.{u} } ⟶
      { X := Option Z.X,
        toTwoPointing := { fst := none, snd := some Z.point, fst_ne_snd := ⋯ : TwoPointing (Option Z.X) } })
    { hom := { toFun := Option.map (f ≫ g).toFun, map_fst := ⋯, map_snd := ⋯ } }
    (CategoryStruct.comp (Y :=
      { X := Option Y.X,
        toTwoPointing := { fst := none, snd := some Y.point, fst_ne_snd := ⋯ : TwoPointing (Option Y.X) } })
      { hom := { toFun := Option.map f.toFun, map_fst := ⋯, map_snd := ⋯ } }
      { hom := { toFun := Option.map g.toFun, map_fst := ⋯, map_snd := ⋯ } })

Tactic:
ext : 3