∀ {I : Type u_4} {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_4} I] [inst_1 : CategoryTheory.IsConnected I]
  [inst_2 : CategoryTheory.Category.{u_1, u_2} C] {F G : CategoryTheory.Functor I C} (α : F ⟶ G)
  (cF : CategoryTheory.Limits.Cone F) (cG : CategoryTheory.Limits.Cone G)
  (f : (CategoryTheory.Limits.Cones.postcompose α).obj cF ⟶ cG)
  (hf : ∀ (i : I), CategoryTheory.IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i))
  (hcG : CategoryTheory.Limits.IsLimit cG) (s : CategoryTheory.Limits.Cone F) (g : s.pt ⟶ cF.pt),
  (∀ (j : I), CategoryTheory.CategoryStruct.comp g (cF.π.app j) = s.π.app j) →
    CategoryTheory.CategoryStruct.comp g (cF.π.app (Classical.arbitrary I)) =
      CategoryTheory.CategoryStruct.comp
        (⋯.lift (s.π.app (Classical.arbitrary I)) (hcG.lift ((CategoryTheory.Limits.Cones.postcompose α).obj s)) ⋯)
        (cF.π.app (Classical.arbitrary I))