-- Lean 4 proof step from Mathlib.CategoryTheory.Category.TwoP (goal)
Goal:
α : Type u_1
β : Type u_2
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
⊢ 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 := ⋯ } })
have h : Eq (α :=
  { X := Option X.X,
          toTwoPointing :=
            { fst := none, snd := some X.point, fst_ne_snd := sorry : TwoPointing (Option X.X) } }.toBipointed.X →
    { X := Option Z.X,
          toTwoPointing :=
            { fst := none, snd := some Z.point, fst_ne_snd := sorry : 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 := sorry, map_snd := sorry :
                { X := Option X.X,
                        toTwoPointing :=
                          { fst := none, snd := some X.point, fst_ne_snd := sorry : TwoPointing (Option X.X) } :
                        TwoP.{u} }.toBipointed.Hom
                  { X := Option Z.X,
                      toTwoPointing :=
                        { fst := none, snd := some Z.point, fst_ne_snd := sorry : 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 := sorry : TwoPointing (Option X.X) } :
                TwoP.{u} }
              { X := Option Z.X,
                toTwoPointing := { fst := none, snd := some Z.point, fst_ne_snd := sorry : TwoPointing (Option Z.X) } :
                TwoP.{u} } })) :
    { X := Option X.X, toTwoPointing := { fst := none, snd := some X.point, fst_ne_snd := sorry } }.toBipointed.X →
      { X := Option Z.X, toTwoPointing := { fst := none, snd := some Z.point, fst_ne_snd := sorry } }.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 := sorry : TwoPointing (Option Y.X) } :
              TwoP.{u} })
            {
              hom :=
                { toFun := Option.map f.toFun, map_fst := sorry, map_snd := sorry :
                  { X := Option X.X,
                          toTwoPointing :=
                            { fst := none, snd := some X.point, fst_ne_snd := sorry : TwoPointing (Option X.X) } :
                          TwoP.{u} }.toBipointed.Hom
                    { X := Option Y.X,
                        toTwoPointing :=
                          { fst := none, snd := some Y.point, fst_ne_snd := sorry : 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 := sorry : TwoPointing (Option X.X) } :
                  TwoP.{u} }
                { X := Option Y.X,
                  toTwoPointing := { fst := none, snd := some Y.point, fst_ne_snd := sorry : TwoPointing (Option Y.X) } :
                  TwoP.{u} } }
            {
              hom :=
                { toFun := Option.map g.toFun, map_fst := sorry, map_snd := sorry :
                  { X := Option Y.X,
                          toTwoPointing :=
                            { fst := none, snd := some Y.point, fst_ne_snd := sorry : TwoPointing (Option Y.X) } :
                          TwoP.{u} }.toBipointed.Hom
                    { X := Option Z.X,
                        toTwoPointing :=
                          { fst := none, snd := some Z.point, fst_ne_snd := sorry : 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 := sorry : TwoPointing (Option Y.X) } :
                  TwoP.{u} }
                { X := Option Z.X,
                  toTwoPointing := { fst := none, snd := some Z.point, fst_ne_snd := sorry : TwoPointing (Option Z.X) } :
                  TwoP.{u} } }))) :
    { X := Option X.X, toTwoPointing := { fst := none, snd := some X.point, fst_ne_snd := sorry } }.toBipointed.X →
      { X := Option Z.X, toTwoPointing := { fst := none, snd := some Z.point, fst_ne_snd := sorry } }.toBipointed.X)
Tactic: ext : 3