-- Module: Mathlib.AlgebraicGeometry.Cover.Over
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
rw :
  (∀ (x : ↥W),
      ∃ (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X x).asOverProp (P := Q) S ⋯) (Z :=
                    X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S)
                    (Hom.asOverProp (P := Q) (𝒰.f x) S))).left,
            f := fun (x : 𝒰.I₀) ↦
              CommaMorphism.left
                (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))) }),
        Membership.mem (γ := Set ↥W)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := 𝒰.I₀,
                  X := fun (x : 𝒰.I₀) ↦
                    (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
                        (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X x).asOverProp (P := Q) S ⋯) (Z :=
                          X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S)
                          (Hom.asOverProp (P := Q) (𝒰.f x) S))).left,
                  f := fun (x : 𝒰.I₀) ↦
                    CommaMorphism.left
                      (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
                        (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))) :
                  PreZeroHypercover.{u_1, u, u + 1} W }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := 𝒰.I₀,
                  X := fun (x : 𝒰.I₀) ↦
                    (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
                        (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X x).asOverProp (P := Q) S ⋯) (Z :=
                          X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S)
                          (Hom.asOverProp (P := Q) (𝒰.f x) S))).left,
                  f := fun (x : 𝒰.I₀) ↦
                    CommaMorphism.left
                      (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
                        (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))) :
                  PreZeroHypercover.{u_1, u, u + 1} W }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X x).asOverProp (P := Q) S ⋯) (Z :=
                    X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S)
                    (Hom.asOverProp (P := Q) (𝒰.f x) S))).left,
            f := fun (x : 𝒰.I₀) ↦
              CommaMorphism.left
                (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))) }),
      P
        (PreZeroHypercover.f
          { I₀ := 𝒰.I₀,
            X := fun (x : 𝒰.I₀) ↦
              (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X x).asOverProp (P := Q) S ⋯) (Z :=
                    X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S)
                    (Hom.asOverProp (P := Q) (𝒰.f x) S))).left,
            f := fun (x : 𝒰.I₀) ↦
              CommaMorphism.left
                (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
                  (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))) :
            PreZeroHypercover.{u_1, u, u + 1} W }
          i)
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1}
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
              (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X x).asOverProp (P := Q) S ⋯) (Z :=
                X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))).left,
        f := fun (x : 𝒰.I₀) ↦
          CommaMorphism.left
            (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
              (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))) } ∈
    (precoverage P).coverings W

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff