∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R₁ R₂ : CategoryTheory.Presieve X} (h : R₁ ≤ R₂) (x : CategoryTheory.Presieve.FamilyOfElements P R₂) (x_1 : C)
  (f : x_1 ⟶ X) (hf : R₁ f), CategoryTheory.Presieve.FamilyOfElements.restrict h x f hf = x f ⋯