-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥(X ⨿ Y)
h :
  ∀ (x : ↥X ⊕ ↥Y),
    Membership.mem (α := ↥(X ⨿ Y)) (γ := 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)
                ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))))))
        ⇑(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)
                ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))))))
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))
⊢ 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

Tactic:
obtain ⟨x, rfl⟩ := (coprodMk X Y).surjective x

Premises used: AlgebraicGeometry.coprodMk, Homeomorph.surjective, rfl