∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.map (CategoryTheory.Functor.id C)).map f)
      ((fun X =>
            match X with
            | CategoryTheory.WithTerminal.of a =>
              CategoryTheory.Iso.refl
                ((CategoryTheory.WithTerminal.map (CategoryTheory.Functor.id C)).obj (CategoryTheory.WithTerminal.of a))
            | CategoryTheory.WithTerminal.star =>
              CategoryTheory.Iso.refl
                ((CategoryTheory.WithTerminal.map (CategoryTheory.Functor.id C)).obj CategoryTheory.WithTerminal.star))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X =>
            match X with
            | CategoryTheory.WithTerminal.of a =>
              CategoryTheory.Iso.refl
                ((CategoryTheory.WithTerminal.map (CategoryTheory.Functor.id C)).obj (CategoryTheory.WithTerminal.of a))
            | CategoryTheory.WithTerminal.star =>
              CategoryTheory.Iso.refl
                ((CategoryTheory.WithTerminal.map (CategoryTheory.Functor.id C)).obj CategoryTheory.WithTerminal.star))
          X).hom
      ((CategoryTheory.Functor.id (CategoryTheory.WithTerminal C)).map f)