-- Module: Mathlib.AlgebraicGeometry.Limits
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)
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 ⋯))
        (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)
⊢ 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))

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 _) ?_

Premises used: CategoryTheory.IsIso.of_isIso_fac_right