∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {ι : Type u_4} {S : C} {X : ι → C}
  {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type u_3} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)},
  (∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p) →
    ∀ ⦃Y : C⦄ (q : Y ⟶ S') ⦃j₁ : ι'⦄ (f₁ : Y ⟶ X' j₁) (q' : Y ⟶ S) (f₁' : Y ⟶ X (α j₁)),
      autoParam (CategoryTheory.CategoryStruct.comp f₁ (f' j₁) = q)
          CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_1 →
        autoParam (CategoryTheory.CategoryStruct.comp q p = q')
            CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_5 →
          autoParam (CategoryTheory.CategoryStruct.comp f₁ (p' j₁) = f₁')
              CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_7 →
            CategoryTheory.CategoryStruct.comp f₁' (f (α j₁)) = q'