-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} X
f : X ⟶ Z
g : Y ⟶ Z
refine_1 :
  ∀ (x : ↥(pullback f g)),
    ∃ (i :
      PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
        { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
          f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }),
      Membership.mem (γ := Set ↥(pullback f g))
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
                f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ :
                PreZeroHypercover.{v, u, u + 1} (pullback f g) }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
                f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ :
                PreZeroHypercover.{v, u, u + 1} (pullback f g) }
              i))
        x
refine_2 :
  ∀
    (i :
      PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
        { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
          f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }),
    IsOpenImmersion
      (PreZeroHypercover.f
        { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
          f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ :
          PreZeroHypercover.{v, u, u + 1} (pullback f g) }
        i)
⊢ (∀ (x : ↥(pullback f g)),
      ∃ (i :
        PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
          { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
            f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }),
        Membership.mem (γ := Set ↥(pullback f g))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
                  f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ :
                  PreZeroHypercover.{v, u, u + 1} (pullback f g) }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
                  f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ :
                  PreZeroHypercover.{v, u, u + 1} (pullback f g) }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
          { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
            f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
            f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ :
            PreZeroHypercover.{v, u, u + 1} (pullback f g) }
          i)

Tactic:
refine ⟨fun x ↦ ?_, fun i ↦ ?_⟩