∀ {I : Type u_5} (C : I → Type u_3) [inst : (i : I) → CategoryTheory.Category.{u_1, u_3} (C i)] {J : Type u_4}
  {K : Type u_2} (f : K → J) (g : J → I) (X Y : (i : I) → C i) (f' : X ⟶ Y),
  (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Pi.comap C g).comp (CategoryTheory.Pi.comap (C ∘ g) f)).map f')
      fun b => CategoryTheory.CategoryStruct.id (Y (g (f b)))) =
    CategoryTheory.CategoryStruct.comp (fun b => CategoryTheory.CategoryStruct.id (X (g (f b))))
      ((CategoryTheory.Pi.comap C (g ∘ f)).map f')