-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ Membership.mem (γ := Set (Presieve (X ⨿ Y))) ((Scheme.precoverage IsOpenImmersion).coverings (X ⨿ Y))
    (PreZeroHypercover.presieve₀.{w, u, u + 1}
      { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1},
        X := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
          Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x,
        f := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
          Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
            (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr) x })
have rw : (∀ (x : ↥(X ⨿ Y)),
    ∃ (i :
      PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := X ⨿ Y)
        { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1},
          X := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x,
          f := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
              (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr) x }),
      Membership.mem (γ := Set ↥(X ⨿ Y))
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1},
                X := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
                  Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x,
                f := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
                  Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
                    Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
                    (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr) x :
                PreZeroHypercover.{w, u, u + 1} (X ⨿ Y) }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1},
                X := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
                  Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x,
                f := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
                  Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
                    Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
                    (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr) x :
                PreZeroHypercover.{w, u, u + 1} (X ⨿ Y) }
              i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := X ⨿ Y)
        { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1},
          X := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x,
          f := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
              (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr) x }),
    IsOpenImmersion
      (PreZeroHypercover.f
        { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1},
          X := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x,
          f := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
              (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr) x :
          PreZeroHypercover.{w, u, u + 1} (X ⨿ Y) }
        i)
Tactic: rw [Scheme.presieve₀_mem_precoverage_iff]