-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
inst_3 : Q.IsStableUnderComposition
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left
h_1 : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
T : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOverProp (P := P) (Q := Q) p f → Presieve Y
V :
  ⦃Y : Q.Over ⊤ S⦄ →
    (f : Y ⟶ X) →
      (H : 𝒰.toPresieveOverProp (P := P) (Q := Q) p f) → Cover (precoverage P) Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left
h : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOverProp (P := P) (Q := Q) p f) → Cover.Over S (P := P) (V f H)
pV :
  ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp (P := P) (Q := Q) p f) (j : (V f H).I₀), Q ((V f H).X j ↘ S)
hV :
  ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp (P := P) (Q := Q) p f),
    T f H = (V f H).toPresieveOverProp (P := P) (Q := Q) ⋯
𝒱j : (j : 𝒰.I₀) → Cover (precoverage P) ((𝒰.X j).asOverProp (P := Q) S ⋯).toComma (P := Q) (Q := ⊤) (W := ⊤).left :=
  fun (j : 𝒰.I₀) ↦ V (Hom.asOverProp (P := Q) (𝒰.f j) S) ⋯
⊢ Eq.{u + 2} (α := Presieve (C := Q.Over ⊤ S) (X.toComma (P := Q) (Q := ⊤) (W := ⊤).left.asOverProp (P := Q) S ⋯))
    (Presieve.bind
      (Presieve.ofArrows (fun (j : 𝒰.I₀) ↦ (𝒰.X j).asOverProp (P := Q) S ⋯) fun (j : 𝒰.I₀) ↦
        Hom.asOverProp (P := Q) (𝒰.f j) S)
      fun (x : Q.Over ⊤ S) (f : x ⟶ X.toComma (P := Q) (Q := ⊤) (W := ⊤).left.asOverProp (P := Q) S ⋯)
        (H :
          Presieve.ofArrows (fun (j : 𝒰.I₀) ↦ (𝒰.X j).asOverProp (P := Q) S ⋯)
            (fun (j : 𝒰.I₀) ↦ Hom.asOverProp (P := Q) (𝒰.f j) S) f) ↦
      Presieve.ofArrows (fun (j : (V f H).I₀) ↦ ((V f H).X j).asOverProp (P := Q) S ⋯) fun (j : (V f H).I₀) ↦
        Hom.asOverProp (P := Q) ((V f H).f j) S)
    (Presieve.ofArrows
      (fun (i : (i : 𝒰.I₀) × (V (Hom.asOverProp (P := Q) (𝒰.f i) S) ⋯).I₀) ↦
        ((V
                  (Hom.asOverProp (P := Q)
                    (𝒰.f (i.fst (β := fun (i : 𝒰.I₀) ↦ (V (Hom.asOverProp (P := Q) (𝒰.f i) S) ⋯).I₀))) S)
                  ⋯).X
              (i.snd (β := fun (i : 𝒰.I₀) ↦ (V (Hom.asOverProp (P := Q) (𝒰.f i) S) ⋯).I₀))).asOverProp
          (P := Q) S ⋯)
      fun (ij : (i : 𝒰.I₀) × (V (Hom.asOverProp (P := Q) (𝒰.f i) S) ⋯).I₀) ↦
      CategoryStruct.comp (Y :=
        (𝒰.X (ij.fst (β := fun (i : 𝒰.I₀) ↦ (V (Hom.asOverProp (P := Q) (𝒰.f i) S) ⋯).I₀))).asOverProp (P := Q) S ⋯)
        (Hom.asOverProp (P := Q)
          ((V
                (Hom.asOverProp (P := Q)
                  (𝒰.f (ij.fst (β := fun (i : 𝒰.I₀) ↦ (V (Hom.asOverProp (P := Q) (𝒰.f i) S) ⋯).I₀))) S)
                ⋯).f
            (ij.snd (β := fun (i : 𝒰.I₀) ↦ (V (Hom.asOverProp (P := Q) (𝒰.f i) S) ⋯).I₀)))
          S)
        (Hom.asOverProp (P := Q) (𝒰.f (ij.fst (β := fun (i : 𝒰.I₀) ↦ (V (Hom.asOverProp (P := Q) (𝒰.f i) S) ⋯).I₀))) S))

Tactic:
Presieve.ofArrows_bind _ (fun j ↦ ((𝒰.f j).asOverProp S)) _
        (fun Y f H j ↦ ((V f H).X j).asOverProp S (pV _ _ _))
        (fun Y f H j ↦ ((V f H).f j).asOverProp S)

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.asOverProp, CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.Scheme.asOverProp, CategoryTheory.Presieve.ofArrows_bind, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover