-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
x : ↥W
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
              (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }),
    Membership.mem (γ := Set ↥W)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := 𝒰.I₀,
              X := fun (x : 𝒰.I₀) ↦
                (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                    (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
              f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
              PreZeroHypercover.{u_1, u, u + 1} W }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := 𝒰.I₀,
              X := fun (x : 𝒰.I₀) ↦
                (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                    (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
              f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
              PreZeroHypercover.{u_1, u, u + 1} W }
            i))
      x
have refine_1 : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀)
  (hy :
    ∃ (y : ↥((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)), ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) y = x),
  ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
              (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }),
    Membership.mem (γ := Set ↥W)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := 𝒰.I₀,
              X := fun (x : 𝒰.I₀) ↦
                (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                    (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
              f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
              PreZeroHypercover.{u_1, u, u + 1} W }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := 𝒰.I₀,
              X := fun (x : 𝒰.I₀) ↦
                (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                    (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
              f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
              PreZeroHypercover.{u_1, u, u + 1} W }
            i))
      x
Tactic: obtain ⟨i, hy⟩ := Cover.exists_eq (𝒰.pullback₁ f) x