-- Module: Mathlib.AlgebraicGeometry.Gluing
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 := (glueData F).U ((equivShrink J : (a : J) → Shrink.{u, w} J) 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))
      ((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:
simp [← Category.assoc, ← Iso.comp_inv_eq, cocone]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, AlgebraicGeometry.Scheme.IsLocallyDirected.cocone