-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
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
have 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))
Tactic: obtain ⟨x, rfl⟩ := (coprodMk X Y).surjective x
Cleared hypotheses: x