-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
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)
⊢ 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 })

Tactic:
rw [Scheme.presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff