-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} X
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀
simp_rw :
  Eq (α := pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g ⟶ limit (cospan f g))
    (pullback.map ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g f g ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i)
      (𝟙 Y) (𝟙 Z) ⋯ ⋯)
    (Iso.hom (Iso.refl (pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g)) ≫
      (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).ι
          (Sigma.snd (β := fun (i : PUnit.{u + 1}) ↦ (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀)
            ((Equiv.trans (Equiv.symm (Equiv.punitProd (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀))
                  (Equiv.symm (Equiv.sigmaEquivProd PUnit.{u + 1} (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀)) :
                (a : (Cover.ulift 𝒰).I₀) → (_ : PUnit.{u + 1}) × (Cover.ulift 𝒰).I₀)
              ((Equiv.refl (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀ : (a : (Cover.ulift 𝒰).I₀) → (Cover.ulift 𝒰).I₀)
                  i :
                (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀))) ≫
        Iso.inv
          (limit.isoLimitCone
            {
              cone :=
                PullbackCone.mk (W := (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).glued)
                  (p1 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) (p2 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) ⋯,
              isLimit := gluedIsLimit (Cover.ulift (P := IsOpenImmersion) 𝒰) f g : LimitCone (cospan f g) }))
⊢ Eq (α :=
    (fun (i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦ pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g)
        i ⟶
      limit (cospan f g))
    ((fun (i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦
        (pullback.map ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g f g
            ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ :
          pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g ⟶ pullback f g))
      i)
    (CategoryStruct.comp (Y :=
      PreZeroHypercover.X (S := limit (cospan f g))
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Cover.pushforwardIso (P := IsOpenImmersion) (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).openCover
            (Iso.inv
              (limit.isoLimitCone
                {
                  cone :=
                    PullbackCone.mk (W := (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).glued)
                      (p1 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) (p2 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) ⋯,
                  isLimit := gluedIsLimit (Cover.ulift (P := IsOpenImmersion) 𝒰) f g : LimitCone (cospan f g) }))))
        ((Equiv.refl (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀ :
            (a : (Cover.ulift 𝒰).I₀) →
              (Cover.pushforwardIso (gluing (Cover.ulift 𝒰) f g).openCover
                  (limit.isoLimitCone
                      { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
                        isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv).I₀)
          i))
      (Iso.hom
        ((fun (x : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦
            (Iso.refl
                ((fun (i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦
                    pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g)
                  x) :
              Iso (C := Scheme)
                ((fun (i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦
                    pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g)
                  x)
                ((fun (i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦
                    pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g)
                  x)))
          i))
      (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Cover.pushforwardIso (P := IsOpenImmersion) (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).openCover
            (Iso.inv
              (limit.isoLimitCone
                {
                  cone :=
                    PullbackCone.mk (W := (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).glued)
                      (p1 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) (p2 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) ⋯,
                  isLimit := gluedIsLimit (Cover.ulift (P := IsOpenImmersion) 𝒰) f g : LimitCone (cospan f g) }))))
        ((Equiv.refl (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀ :
            (a : (Cover.ulift 𝒰).I₀) →
              (Cover.pushforwardIso (gluing (Cover.ulift 𝒰) f g).openCover
                  (limit.isoLimitCone
                      { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
                        isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv).I₀)
          i)))

Tactic:
simp_rw [Cover.pushforwardIso_I₀, Cover.pushforwardIso_f, GlueData.openCover_f,
          GlueData.openCover_I₀, gluing_J]

Premises used: AlgebraicGeometry.Scheme.GlueData.openCover_f, AlgebraicGeometry.Scheme.Pullback.gluing_J, AlgebraicGeometry.Scheme.Cover.pushforwardIso_f, AlgebraicGeometry.Scheme.Cover.pushforwardIso_I₀, AlgebraicGeometry.Scheme.GlueData.openCover_I₀