-- 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} Z
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ Eq (α :=
    pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ⟶
      pullback f g)
    (pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i))
      (pullback.fst g (𝒰.f i)) (𝒰.f i) ⋯ ⋯)
    (Iso.hom
        (Iso.refl
          ((fun (i : 𝒰.I₀) ↦
              pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i))
                (pullback.snd g (𝒰.f i)))
            i)) ≫
      (openCoverOfBase' 𝒰 f g).f
        ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀)) (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
            (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
          i))
have rw : Eq (α :=
  pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ⟶
    pullback f g)
  (pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
    (𝒰.f i) sorry sorry)
  (Iso.hom
      (pullbackSymmetry
        (pullback.snd f
          (𝒰.f
            (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
              ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀)) (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                  (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                i))))
        (pullback.snd g
          (𝒰.f
            (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
              ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀)) (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                  (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                i))))) ≫
    CategoryStruct.comp (Y :=
      limit
        (cospan (X :=
          pullback (Y :=
            𝒰.X
              (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                      (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                    (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                  i)))
            f
            (𝒰.f
              (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                      (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                    (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                  i))))
          (pullback.snd f
              (𝒰.f
                (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                  ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                        (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                      (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                    i))) ≫
            𝒰.f
              (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                      (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                    (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                  i)))
          g))
      (Iso.inv (limit.isoLimitCone { cone := IsPullback.cone sorry, isLimit := IsPullback.isLimit sorry }))
      (CategoryStruct.comp (Y :=
        pullback (X :=
          pullback (Y :=
            𝒰.X
              (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                      (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                    (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                  i)))
            f
            (𝒰.f
              (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                      (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                    (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                  i))))
          (pullback.fst f
              (𝒰.f
                (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                  ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                        (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                      (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                    i))) ≫
            f)
          g)
        (pullback.map
          (pullback.snd f
              (𝒰.f
                (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                  ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                        (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                      (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                    i))) ≫
            𝒰.f
              (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                      (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                    (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                  i)))
          g
          (pullback.fst f
              (𝒰.f
                (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                  ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                        (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                      (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                    i))) ≫
            f)
          g
          (𝟙
            (pullback (Y :=
              𝒰.X
                (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                  ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                        (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                      (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                    i)))
              f
              (𝒰.f
                (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                  ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                        (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                      (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                    i)))))
          (𝟙 Y) (𝟙 Z) sorry sorry)
        (pullback.map
          (pullback.fst f
              (𝒰.f
                (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                  ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                        (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                      (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                    i))) ≫
            f)
          g f g
          (pullback.fst f
            (𝒰.f
              (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                      (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                    (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                  i))))
          (𝟙 Y) (𝟙 Z) sorry sorry)))
Tactic: rw [Iso.refl_hom, Category.id_comp, openCoverOfBase'_f]