-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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₀
⊢ 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)))
have 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) sorry sorry)
  (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) sorry,
            isLimit := gluedIsLimit (Cover.ulift (P := IsOpenImmersion) 𝒰) f g : LimitCone (cospan f g) }))
Tactic: simp_rw [Cover.pushforwardIso_I₀, Cover.pushforwardIso_f, GlueData.openCover_f,
          GlueData.openCover_I₀, gluing_J]