-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
x : ↥(∐ f)
y :
  ↥(PreZeroHypercover.X (S := colimit (Discrete.functor f))
      (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
        PreZeroHypercover (colimit (Discrete.functor f)))
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x :
        PreZeroHypercover.I₀ (S := colimit (Discrete.functor f))
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
            PreZeroHypercover (colimit (Discrete.functor f)))))
hy :
  (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
right :
  Eq (α := ↥X)
    ((Sigma.desc α)
        ((PreZeroHypercover.f
              (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
              (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
            y :
          ↥(colimit (Discrete.functor f))) :
      ↥X)
    ((α (Discrete.as (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))) y : ↥X)
⊢ IsIso (X :=
    X.presheaf.stalk
      ((Sigma.desc α)
        ((PreZeroHypercover.f
              (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
              (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
            y :
          ↥(colimit (Discrete.functor f)))))
    (Scheme.Hom.stalkMap (Sigma.desc α)
      ((PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y))
have right₁ : Eq (α :=
  X.presheaf.stalk
      ((Sigma.desc α)
        ((PreZeroHypercover.f
              (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
              (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
            y :
          ↥(colimit (Discrete.functor f)))) ⟶
    (PreZeroHypercover.X (S := colimit (Discrete.functor f))
            (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
              PreZeroHypercover (colimit (Discrete.functor f)))
            (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x :
              PreZeroHypercover.I₀ (S := colimit (Discrete.functor f))
                (Precoverage.ZeroHypercover.toPreZeroHypercover
                    (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
                  PreZeroHypercover (colimit (Discrete.functor f))))).presheaf.stalk
      y)
  (Scheme.Hom.stalkMap (Sigma.desc α)
        ((PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
            (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
          y) ≫
      Scheme.Hom.stalkMap
        (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y :
    X.presheaf.stalk
        ((Sigma.desc α)
          ((PreZeroHypercover.f
                (Precoverage.ZeroHypercover.toPreZeroHypercover
                  (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
                (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
              y :
            ↥(colimit (Discrete.functor f)))) ⟶
      (PreZeroHypercover.X (S := colimit (Discrete.functor f))
              (Precoverage.ZeroHypercover.toPreZeroHypercover
                  (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
                PreZeroHypercover (colimit (Discrete.functor f)))
              (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x :
                PreZeroHypercover.I₀ (S := colimit (Discrete.functor f))
                  (Precoverage.ZeroHypercover.toPreZeroHypercover
                      (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
                    PreZeroHypercover (colimit (Discrete.functor f))))).presheaf.stalk
        y)
  (CategoryStruct.comp (Y :=
      X.presheaf.stalk
        ((α (Discrete.as (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))) y))
      (Iso.hom (X.presheaf.stalkCongr sorry))
      (Scheme.Hom.stalkMap
        (α (Discrete.as (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))) y) :
    X.presheaf.stalk
        ((Sigma.desc α)
          ((PreZeroHypercover.f
                (Precoverage.ZeroHypercover.toPreZeroHypercover
                  (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
                (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
              y :
            ↥(colimit (Discrete.functor f)))) ⟶
      (PreZeroHypercover.X (S := colimit (Discrete.functor f))
              (Precoverage.ZeroHypercover.toPreZeroHypercover
                  (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
                PreZeroHypercover (colimit (Discrete.functor f)))
              (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x :
                PreZeroHypercover.I₀ (S := colimit (Discrete.functor f))
                  (Precoverage.ZeroHypercover.toPreZeroHypercover
                      (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
                    PreZeroHypercover (colimit (Discrete.functor f))))).presheaf.stalk
        y)
Tactic: refine IsIso.of_isIso_fac_right
      (f := ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f _).stalkMap y)
      (h := (X.presheaf.stalkCongr (.of_eq ?_)).hom ≫ (α _).stalkMap _) ?_