-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥(X ⨿ Y)
h :
  Membership.mem (γ := Set ↥(X ⨿ Y))
    (Set.range (ι :=
      ↥(PreZeroHypercover.X.{w, u, u + 1} (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 :
            PreZeroHypercover.{w, u, u + 1} (X ⨿ Y) }
          (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
            (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y) x))))
      ⇑(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 }
          (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
            (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y) x))))
    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 }),
    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

Tactic:
use ((coprodMk X Y).symm x).elim (fun _ ↦ Sum.inl .unit) (fun _ ↦ Sum.inr .unit)

Premises used: AlgebraicGeometry.coprodMk, Sum.inl, Sum.inr, Homeomorph.symm, DFunLike.coe, Sum.elim