-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : OpenCover.{u_1, u} Y
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
⊢ (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ≫
      (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).f i =
    CategoryStruct.comp (Y :=
      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X
        (i.fst (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))))
      (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁
              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f
                (i.fst (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                    ((fun (i : 𝒰.I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                          PreZeroHypercover (𝒰.X i)))
                      i))))
              (𝒰.X
                  (i.fst (β := fun (i : 𝒰.I₀) ↦
                    PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                      ((fun (i : 𝒰.I₀) ↦
                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                              ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                            PreZeroHypercover (𝒰.X i)))
                        i)))).affineCover))
          (i.snd (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))) :
        PreZeroHypercover.X
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (Precoverage.ZeroHypercover.pullback₁
                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f
                  (i.fst (β := fun (i : 𝒰.I₀) ↦
                    PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                      ((fun (i : 𝒰.I₀) ↦
                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                              ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                            PreZeroHypercover (𝒰.X i)))
                        i))))
                (𝒰.X
                    (i.fst (β := fun (i : 𝒰.I₀) ↦
                      PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                        ((fun (i : 𝒰.I₀) ↦
                            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                                ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                              PreZeroHypercover (𝒰.X i)))
                          i)))).affineCover))
            (i.snd (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i))) ⟶
          (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i))))
      ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f
          (i.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))) :
        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i))) ⟶
          X)
have simp : Eq (α :=
  pullback (X :=
      pullback (X :=
        𝒰.X
          (i.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
        (𝒰.f
          (i.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
        f)
      (pullback.fst
        (𝒰.f
          (i.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
        f)
      (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (𝒰.X
              (i.fst (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (S := 𝒰.X i)
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))).affineCover)
        (i.snd (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))) ⟶
    X)
  (CategoryStruct.comp (Y :=
      pullback (Y :=
        pullback (X :=
          𝒰.X
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f)
        (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒰.X
                (i.fst (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (S := 𝒰.X i)
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))).affineCover)
          (i.snd (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
        (pullback.fst
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f))
      (Iso.inv
        (pullbackSymmetry
          (PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (𝒰.X
                  (i.fst (β := fun (i : 𝒰.I₀) ↦
                    PreZeroHypercover.I₀ (S := 𝒰.X i)
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))).affineCover)
            (i.snd (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          (pullback.fst
            (𝒰.f
              (i.fst (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (S := 𝒰.X i)
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
            f)))
      (Iso.hom
          (pullbackRightPullbackFstIso
            (𝒰.f
              (i.fst (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (S := 𝒰.X i)
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
            f
            (PreZeroHypercover.f
              (Precoverage.ZeroHypercover.toPreZeroHypercover
                (𝒰.X
                    (i.fst (β := fun (i : 𝒰.I₀) ↦
                      PreZeroHypercover.I₀ (S := 𝒰.X i)
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))).affineCover)
              (i.snd (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (S := 𝒰.X i)
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))) ≫
        pullback.snd (𝒰.affineRefinement.f (P := IsOpenImmersion) i) f) :
    pullback (X :=
        pullback (X :=
          𝒰.X
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f)
        (pullback.fst
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f)
        (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒰.X
                (i.fst (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (S := 𝒰.X i)
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))).affineCover)
          (i.snd (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))) ⟶
      X)
  (pullback.fst
        (pullback.fst
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f)
        (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒰.X
                (i.fst (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (S := 𝒰.X i)
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))).affineCover)
          (i.snd (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))) ≫
      pullback.snd
        (𝒰.f
          (i.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
        f :
    pullback (X :=
        pullback (X :=
          𝒰.X
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f)
        (pullback.fst
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f)
        (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒰.X
                (i.fst (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (S := 𝒰.X i)
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))).affineCover)
          (i.snd (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))) ⟶
      X)
Tactic: simp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
    PreZeroHypercover.pullback₁_X, AffineOpenCover.openCover_X, AffineOpenCover.openCover_f,
    pullbackCoverAffineRefinementObjIso, Iso.trans_inv, asIso_inv, Iso.symm_inv, Category.assoc,
    PreZeroHypercover.pullback₁_f, pullbackSymmetry_inv_comp_fst, IsIso.inv_comp_eq,
    limit.lift_π_assoc, PullbackCone.mk_pt, cospan_left, PullbackCone.mk_π_app,
    pullbackSymmetry_hom_comp_fst]