-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
i : J
⊢ Eq (α := F.obj i ⟶ Limits.colimit F) (colimit.ι F i)
    (CategoryStruct.comp (Y :=
      PreZeroHypercover.X (S := Limits.colimit F)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
          (Precoverage.ZeroHypercover.bind
            (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
              (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))))
            fun
              (i :
                PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                      (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
            (glueData F).openCover))
        ((Equiv.trans (β := Shrink.{u, w} J) (equivShrink J)
              (Equiv.symm (Equiv.uniqueSigma fun (x : Unit) ↦ Shrink.{u, w} J)) :
            (a : J) →
              (Precoverage.ZeroHypercover.bind
                  (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom)
                  fun (i : (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom).I₀) ↦
                  (glueData F).openCover).I₀)
          i))
      (Iso.hom
        ((fun (x : J) ↦
            (F.mapIso (eqToIso ⋯) :
              F.obj x ≅
                F.obj
                  ↓(Sigma.snd (β :=
                        fun
                          (i :
                            PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                  (Iso.hom
                                    (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
                        PreZeroHypercover.I₀ (C := Scheme) (S :=
                          PreZeroHypercover.X
                            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                              (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                            i)
                          ((fun
                                (i :
                                  PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                      (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                        (Iso.hom
                                          (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
                              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                  ((fun
                                        (i :
                                          PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                            (Precoverage.ZeroHypercover.toPreZeroHypercover (J :=
                                              precoverage IsOpenImmersion)
                                              (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                                (Iso.hom
                                                  (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                                    (colimit.isColimit F)))))) ↦
                                      ((glueData F).openCover : (glueData F).glued.OpenCover))
                                    i) :
                                PreZeroHypercover
                                  (PreZeroHypercover.X
                                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                      (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                        (Iso.hom
                                          (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                                    i)))
                            i))
                        ((Equiv.trans (β := Shrink.{u, w} J) (equivShrink J)
                              (Equiv.symm (Equiv.uniqueSigma fun (x : Unit) ↦ Shrink.{u, w} J)) :
                            (a : J) →
                              (Precoverage.ZeroHypercover.bind
                                  (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom)
                                  fun
                                    (i :
                                      (coverOfIsIso
                                          ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom).I₀) ↦
                                  (glueData F).openCover).I₀)
                          x) :
                      PreZeroHypercover.I₀ (C := Scheme) (S :=
                        PreZeroHypercover.X (S := (colimit.cocone F).pt)
                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                              (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                          (Sigma.fst (β :=
                            fun
                              (i :
                                PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                    (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                      (Iso.hom
                                        (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
                            PreZeroHypercover.I₀ (C := Scheme) (S :=
                              PreZeroHypercover.X
                                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                  (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                    (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                                i)
                              ((fun
                                    (i :
                                      PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J :=
                                          precoverage IsOpenImmersion)
                                          (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                            (Iso.hom
                                              (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                                (colimit.isColimit F)))))) ↦
                                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                      ((fun
                                            (i :
                                              PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                                (Precoverage.ZeroHypercover.toPreZeroHypercover (J :=
                                                  precoverage IsOpenImmersion)
                                                  (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                                    (Iso.hom
                                                      (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                                        (colimit.isColimit F)))))) ↦
                                          ((glueData F).openCover : (glueData F).glued.OpenCover))
                                        i) :
                                    PreZeroHypercover
                                      (PreZeroHypercover.X
                                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J :=
                                          precoverage IsOpenImmersion)
                                          (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                            (Iso.hom
                                              (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                                (colimit.isColimit F)))))
                                        i)))
                                i))
                            ((Equiv.trans (β := Shrink.{u, w} J) (equivShrink J)
                                  (Equiv.symm (Equiv.uniqueSigma fun (x : Unit) ↦ Shrink.{u, w} J)) :
                                (a : J) →
                                  (Precoverage.ZeroHypercover.bind
                                      (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom)
                                      fun
                                        (i :
                                          (coverOfIsIso
                                              ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom).I₀) ↦
                                      (glueData F).openCover).I₀)
                              x)))
                        ((fun
                              (i :
                                PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                    (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                      (Iso.hom
                                        (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
                            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                ((fun
                                      (i :
                                        PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J :=
                                            precoverage IsOpenImmersion)
                                            (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                              (Iso.hom
                                                (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                                  (colimit.isColimit F)))))) ↦
                                    ((glueData F).openCover : (glueData F).glued.OpenCover))
                                  i) :
                              PreZeroHypercover
                                (PreZeroHypercover.X
                                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                    (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                      (Iso.hom
                                        (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                                  i)))
                          (Sigma.fst (β :=
                            fun
                              (i :
                                PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                    (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                      (Iso.hom
                                        (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
                            PreZeroHypercover.I₀ (C := Scheme) (S :=
                              PreZeroHypercover.X
                                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                  (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                    (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                                i)
                              ((fun
                                    (i :
                                      PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J :=
                                          precoverage IsOpenImmersion)
                                          (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                            (Iso.hom
                                              (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                                (colimit.isColimit F)))))) ↦
                                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                      ((fun
                                            (i :
                                              PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                                (Precoverage.ZeroHypercover.toPreZeroHypercover (J :=
                                                  precoverage IsOpenImmersion)
                                                  (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                                    (Iso.hom
                                                      (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                                        (colimit.isColimit F)))))) ↦
                                          ((glueData F).openCover : (glueData F).glued.OpenCover))
                                        i) :
                                    PreZeroHypercover
                                      (PreZeroHypercover.X
                                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J :=
                                          precoverage IsOpenImmersion)
                                          (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                            (Iso.hom
                                              (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                                (colimit.isColimit F)))))
                                        i)))
                                i))
                            ((Equiv.trans (β := Shrink.{u, w} J) (equivShrink J)
                                  (Equiv.symm (Equiv.uniqueSigma fun (x : Unit) ↦ Shrink.{u, w} J)) :
                                (a : J) →
                                  (Precoverage.ZeroHypercover.bind
                                      (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom)
                                      fun
                                        (i :
                                          (coverOfIsIso
                                              ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom).I₀) ↦
                                      (glueData F).openCover).I₀)
                              x))))))
          i))
      (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
          (Precoverage.ZeroHypercover.bind
            (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
              (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F))))
            fun
              (i :
                PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                      (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
            (glueData F).openCover))
        ((Equiv.trans (β := Shrink.{u, w} J) (equivShrink J)
              (Equiv.symm (Equiv.uniqueSigma fun (x : Unit) ↦ Shrink.{u, w} J)) :
            (a : J) →
              (Precoverage.ZeroHypercover.bind
                  (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom)
                  fun (i : (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom).I₀) ↦
                  (glueData F).openCover).I₀)
          i)))
have change : Eq (α := F.obj i ⟶ Limits.colimit F) (colimit.ι F i)
  (CategoryStruct.comp (Y := (glueData F).U ((equivShrink J : (a : J) → Shrink.{u, w} J) i))
    (Iso.hom
      ((fun (x : J) ↦
          (F.mapIso (eqToIso sorry) :
            F.obj x ≅
              F.obj
                ↓(Sigma.snd (β :=
                      fun
                        (i :
                          PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                              (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
                      PreZeroHypercover.I₀ (C := Scheme) (S :=
                        PreZeroHypercover.X
                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                              (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                          i)
                        ((fun
                              (i :
                                PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                    (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                      (Iso.hom
                                        (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
                            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                ((fun
                                      (i :
                                        PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J :=
                                            precoverage IsOpenImmersion)
                                            (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                              (Iso.hom
                                                (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                                  (colimit.isColimit F)))))) ↦
                                    ((glueData F).openCover : (glueData F).glued.OpenCover))
                                  i) :
                              PreZeroHypercover
                                (PreZeroHypercover.X
                                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                    (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                      (Iso.hom
                                        (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                                  i)))
                          i))
                      ((Equiv.trans (β := Shrink.{u, w} J) (equivShrink J)
                            (Equiv.symm (Equiv.uniqueSigma fun (x : Unit) ↦ Shrink.{u, w} J)) :
                          (a : J) →
                            (Precoverage.ZeroHypercover.bind
                                (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom)
                                fun
                                  (i :
                                    (coverOfIsIso
                                        ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom).I₀) ↦
                                (glueData F).openCover).I₀)
                        x) :
                    PreZeroHypercover.I₀ (C := Scheme) (S :=
                      PreZeroHypercover.X (S := (colimit.cocone F).pt)
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                            (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                        (Sigma.fst (β :=
                          fun
                            (i :
                              PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                  (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                    (Iso.hom
                                      (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
                          PreZeroHypercover.I₀ (C := Scheme) (S :=
                            PreZeroHypercover.X
                              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                  (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                              i)
                            ((fun
                                  (i :
                                    PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                        (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                          (Iso.hom
                                            (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                              (colimit.isColimit F)))))) ↦
                                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                    ((fun
                                          (i :
                                            PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                              (Precoverage.ZeroHypercover.toPreZeroHypercover (J :=
                                                precoverage IsOpenImmersion)
                                                (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                                  (Iso.hom
                                                    (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                                      (colimit.isColimit F)))))) ↦
                                        ((glueData F).openCover : (glueData F).glued.OpenCover))
                                      i) :
                                  PreZeroHypercover
                                    (PreZeroHypercover.X
                                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                        (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                          (Iso.hom
                                            (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                                      i)))
                              i))
                          ((Equiv.trans (β := Shrink.{u, w} J) (equivShrink J)
                                (Equiv.symm (Equiv.uniqueSigma fun (x : Unit) ↦ Shrink.{u, w} J)) :
                              (a : J) →
                                (Precoverage.ZeroHypercover.bind
                                    (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom)
                                    fun
                                      (i :
                                        (coverOfIsIso
                                            ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom).I₀) ↦
                                    (glueData F).openCover).I₀)
                            x)))
                      ((fun
                            (i :
                              PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                  (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                    (Iso.hom
                                      (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                              ((fun
                                    (i :
                                      PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J :=
                                          precoverage IsOpenImmersion)
                                          (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                            (Iso.hom
                                              (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                                (colimit.isColimit F)))))) ↦
                                  ((glueData F).openCover : (glueData F).glued.OpenCover))
                                i) :
                            PreZeroHypercover
                              (PreZeroHypercover.X
                                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                  (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                    (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                                i)))
                        (Sigma.fst (β :=
                          fun
                            (i :
                              PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                  (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                    (Iso.hom
                                      (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
                          PreZeroHypercover.I₀ (C := Scheme) (S :=
                            PreZeroHypercover.X
                              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                  (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                              i)
                            ((fun
                                  (i :
                                    PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                        (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                          (Iso.hom
                                            (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                              (colimit.isColimit F)))))) ↦
                                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                    ((fun
                                          (i :
                                            PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                                              (Precoverage.ZeroHypercover.toPreZeroHypercover (J :=
                                                precoverage IsOpenImmersion)
                                                (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                                  (Iso.hom
                                                    (IsColimit.coconePointUniqueUpToIso (isColimit F)
                                                      (colimit.isColimit F)))))) ↦
                                        ((glueData F).openCover : (glueData F).glued.OpenCover))
                                      i) :
                                  PreZeroHypercover
                                    (PreZeroHypercover.X
                                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                        (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                          (Iso.hom
                                            (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                                      i)))
                              i))
                          ((Equiv.trans (β := Shrink.{u, w} J) (equivShrink J)
                                (Equiv.symm (Equiv.uniqueSigma fun (x : Unit) ↦ Shrink.{u, w} J)) :
                              (a : J) →
                                (Precoverage.ZeroHypercover.bind
                                    (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom)
                                    fun
                                      (i :
                                        (coverOfIsIso
                                            ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom).I₀) ↦
                                    (glueData F).openCover).I₀)
                            x))))))
        i))
    ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) i) ≫
      PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
          (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
            (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
        (Sigma.fst (β :=
          fun
            (i :
              PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                  (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                    (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S :=
            PreZeroHypercover.X
              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                  (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
              i)
            ((fun
                  (i :
                    PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                          (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun
                          (i :
                            PreZeroHypercover.I₀ (S := (colimit.cocone F).pt)
                              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                                  (Iso.hom
                                    (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))) ↦
                        ((glueData F).openCover : (glueData F).glued.OpenCover))
                      i) :
                  PreZeroHypercover
                    (PreZeroHypercover.X
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        (coverOfIsIso (P := IsOpenImmersion) (X := (cocone F).pt)
                          (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) (colimit.isColimit F)))))
                      i)))
              i))
          ((Equiv.trans (β := Shrink.{u, w} J) (equivShrink J)
                (Equiv.symm (Equiv.uniqueSigma fun (x : Unit) ↦ Shrink.{u, w} J)) :
              (a : J) →
                (Precoverage.ZeroHypercover.bind
                    (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom)
                    fun (i : (coverOfIsIso ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).hom).I₀) ↦
                    (glueData F).openCover).I₀)
            i))))
Tactic: change colimit.ι F i = _ ≫ (glueData F).ι (equivShrink J i) ≫ _