∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {T : Type u_2}
  (F : CategoryTheory.Functor C (CategoryTheory.Discrete T)) (t : T) [inst_1 : Subsingleton T]
  (X : CategoryTheory.StructuredArrow { as := t } F),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.StructuredArrow.proj { as := t } F).map
        ((CategoryTheory.NatIso.ofComponents
                (fun x =>
                  CategoryTheory.StructuredArrow.isoMk
                    (CategoryTheory.Iso.refl
                      ((CategoryTheory.Functor.id (CategoryTheory.StructuredArrow { as := t } F)).obj x).right)
                    ⋯)
                ⋯).hom.app
          X))
      ((CategoryTheory.Iso.refl
              ({ obj := fun X => CategoryTheory.StructuredArrow.mk (CategoryTheory.eqToHom ⋯),
                    map := fun {X Y} f => CategoryTheory.StructuredArrow.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp
                (CategoryTheory.StructuredArrow.proj { as := t } F))).hom.app
        ((CategoryTheory.StructuredArrow.proj { as := t } F).obj X)) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.StructuredArrow.proj { as := t } F).obj X)