-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this :
  Membership.mem (α := Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))) (γ :=
    Set (Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i)))))
    ((J.over (X i) : (a : Over (X i)) → Set (Sieve a)) (Over.mk (𝟙 (X i))))
    ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
          (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
        (Sieve.pullback (f i) (Sieve.ofArrows X' f')) :
      Sieve (C := Over.{v, u} (X i)) (Over.mk (𝟙 (X i))))
_i :
  ∀ ⦃Y : Over.{v, u} (X i)⦄ ⦃f_1 : Y ⟶ Over.mk (𝟙 (X i))⦄,
    Sieve.arrows
        ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 (X i)))) :
            (a : Sieve (Over.mk (𝟙 (X i))).left) → Sieve (Over.mk (𝟙 (X i))))
          (Sieve.pullback (f i) (Sieve.ofArrows X' f')))
        f_1 →
      Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map f_1.op) :
              (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))) →
                (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y)))
            ((F.presheafHomObjHomEquiv :
                  (a : D₁.obj i ⟶ D₂.obj i) → (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
                (φ.hom i) :
              (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i))))) :
          (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map f_1.op) :
              (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))) →
                (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y)))
            ((F.presheafHomObjHomEquiv :
                  (a : D₁.obj i ⟶ D₂.obj i) → (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
                (φ'.hom i) :
              (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i))))) :
          (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y)))
⊢ Eq (α := (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
    ((F.presheafHomObjHomEquiv :
          (a : D₁.obj i ⟶ D₂.obj i) → (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
        (φ.hom i) :
      (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
    ((F.presheafHomObjHomEquiv :
          (a : D₁.obj i ⟶ D₂.obj i) → (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))
        (φ'.hom i) :
      (F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op (Over.mk (𝟙 (X i)))))

Tactic:
refine (((isSheaf_iff_isSheaf_of_type _ _).1
      (IsPrestack.isSheaf _ _ _)).isSeparated _ this).ext ?_

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.Pseudofunctor.IsPrestack.isSheaf, Iff.mp, CategoryTheory.Presieve.IsSheaf.isSeparated