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