-- 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
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H :
  Membership.mem (α := Sieve (Over.mk f₁)) (γ := Set (Sieve (Over.mk f₁)))
    ((J.over (X i₁) : (a : Over (X i₁)) → Set (Sieve a)) (Over.mk f₁))
    (((Sieve.overEquiv (Over.mk f₁)).symm : (a : Sieve (Over.mk f₁).left) → Sieve (Over.mk f₁))
        (Sieve.pullback q (Sieve.ofArrows X' f')) :
      Sieve (Over.mk f₁))
T : Over.{v, u} (X i₁)
p : T ⟶ Over.mk f₁
Y : C
j : ι'
g : Functor.obj (Over.forget (X i₁)) T ⟶ X' j
fac : g ≫ f' j = Functor.map (Over.forget (X i₁)) p ≫ q
obtain :
  ∀ (T : C) (t : T ⟶ X i₁) ⦃p : Over.mk t ⟶ Over.mk f₁⦄ (g : Functor.obj (Over.forget (X i₁)) (Over.mk t) ⟶ X' j)
    (fac : g ≫ f' j = Functor.map (Over.forget (X i₁)) p ≫ q),
    Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op (Over.mk t))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).map p.op) :
            (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op (Over.mk f₁)))) →
              (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op (Over.mk t))))
          (Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (hom w hf' φ i₁)) :
        (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op (Over.mk t))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).map p.op) :
            (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op (Over.mk f₁)))) →
              (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op (Over.mk t))))
          (D₁.hom q f₁ f₂ ⋯ ⋯ ≫
            Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (hom w hf' φ i₂) ≫ D₂.hom q f₂ f₁ ⋯ ⋯) :
        (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op (Over.mk t))))
⊢ Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op T)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).map p.op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op (Over.mk f₁)))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op T)))
        (Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (hom w hf' φ i₁)) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op T)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).map p.op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op (Over.mk f₁)))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op T)))
        (D₁.hom q f₁ f₂ ⋯ ⋯ ≫
          Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (hom w hf' φ i₂) ≫ D₂.hom q f₂ f₁ ⋯ ⋯) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).obj (op T)))

Tactic:
obtain ⟨T, t, rfl⟩ := T.mk_surjective

Premises used: CategoryTheory.Over.mk_surjective, rfl