-- 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
x : J
⊢ x =
    ↓(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))))

Tactic:
simp [GlueData.openCover, glueData]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.glueData, AlgebraicGeometry.Scheme.GlueData.openCover