-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ (∀ (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:
⟨fun x ↦ ?_, fun x ↦ x.rec (fun _ ↦ inferInstance) (fun _ ↦ inferInstance)⟩

Premises used: And.intro, Sum.rec