-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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
R : Sieve X
Y : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Q.Over ⊤ S
f : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Y x ⟶ X
y : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → ↥(Y x).toComma (P := Q) (Q := ⊤) (W := ⊤).left
hf : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), R.arrows (f x)
hP : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), P (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left
hy : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (y x) = x
⊢ Membership.mem (γ := Set (Presieve X.toComma (P := Q) (Q := ⊤) (W := ⊤).left))
    ((precoverage P).coverings X.toComma (P := Q) (Q := ⊤) (W := ⊤).left)
    (PreZeroHypercover.presieve₀
      { I₀ := ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left,
        X := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (Y i).toComma (P := Q) (Q := ⊤) (W := ⊤).left,
        f := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦
          (f i).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left })
have rw : (∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
    ∃ (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X.toComma (P := Q) (Q := ⊤) (W := ⊤).left)
        { I₀ := ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left,
          X := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (Y i).toComma (P := Q) (Q := ⊤) (W := ⊤).left,
          f := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦
            (f i).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left }),
      Membership.mem (γ := Set ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left,
                X := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦
                  (Y i).toComma (P := Q) (Q := ⊤) (W := ⊤).left,
                f := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦
                  (f i).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left :
                PreZeroHypercover X.toComma (P := Q) (Q := ⊤) (W := ⊤).left }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left,
                X := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦
                  (Y i).toComma (P := Q) (Q := ⊤) (W := ⊤).left,
                f := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦
                  (f i).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left :
                PreZeroHypercover X.toComma (P := Q) (Q := ⊤) (W := ⊤).left }
              i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X.toComma (P := Q) (Q := ⊤) (W := ⊤).left)
        { I₀ := ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left,
          X := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (Y i).toComma (P := Q) (Q := ⊤) (W := ⊤).left,
          f := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦
            (f i).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left }),
    P
      (PreZeroHypercover.f
        { I₀ := ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left,
          X := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (Y i).toComma (P := Q) (Q := ⊤) (W := ⊤).left,
          f := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦
            (f i).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left :
          PreZeroHypercover X.toComma (P := Q) (Q := ⊤) (W := ⊤).left }
        i)
Tactic: rw [presieve₀_mem_precoverage_iff]