-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
e₁ : pullback (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i ≫ toSpecZero 𝒜)
    (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j ≫ toSpecZero 𝒜) ≅
  Spec
    (CommRingCat.of
      (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
        Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) :=
  congrHom ⋯ ⋯ ≪≫
    pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))
      (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))
e₂ : pullback (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i)
    (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j) ≅
  Spec
    (CommRingCat.of
      (Away 𝒜
        ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
    Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) →+*
  Away 𝒜 ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)) :=
  AlgHom.toRingHom
    (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯ :
      Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
          Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) →ₐ[↥(𝒜 0)]
        Away 𝒜
          ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
this :
  Function.Surjective (α :=
    Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
      Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))
    (β :=
    Away 𝒜 ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
    (⇑F : (a : Away 𝒜 (↑i.snd : A) ⊗[↥(𝒜 0)] Away 𝒜 (↑j.snd : A)) → Away 𝒜 ((↑i.snd : A) * (↑j.snd : A)))
⊢ Eq (α :=
    Spec
        (CommRingCat.of
          (Away 𝒜
            ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) *
              (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))) ⟶
      Spec (CommRingCat.of (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (CommRingCat.of (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))) (Y :=
        Spec (CommRingCat.of (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))) (Z :=
        Spec (CommRingCat.of ↥(𝒜 0)))
        (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
        (Spec.map
          (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))))
      ((e₂.inv ≫
          CategoryStruct.comp (Y :=
              pullback (X := Proj 𝒜) (Y :=
                pullback (X := Spec (AffineCover.X (P := IsOpenImmersion) (affineOpenCover 𝒜) i)) (Y :=
                  Spec (AffineCover.X (P := IsOpenImmersion) (affineOpenCover 𝒜) j))
                  (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯ ≫ toSpecZero 𝒜)
                  (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯ ≫ toSpecZero 𝒜))
                (Z := diagonalObj (X := Proj 𝒜) (toSpecZero 𝒜)) (diagonal (toSpecZero 𝒜))
                (pullback.map (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯ ≫ toSpecZero 𝒜)
                  (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯ ≫ toSpecZero 𝒜) (toSpecZero 𝒜)
                  (toSpecZero 𝒜) (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯)
                  (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯) (𝟙 (Spec (CommRingCat.of ↥(𝒜 0)))) ⋯
                  ⋯))
              (Iso.inv
                (pullbackDiagonalMapIdIso (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯)
                  (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯) (toSpecZero 𝒜)))
              (snd (diagonal (toSpecZero 𝒜))
                (pullback.map (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯ ≫ toSpecZero 𝒜)
                  (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯ ≫ toSpecZero 𝒜) (toSpecZero 𝒜)
                  (toSpecZero 𝒜) (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯)
                  (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯) (𝟙 (Spec (CommRingCat.of ↥(𝒜 0)))) ⋯
                  ⋯)) ≫
            e₁.hom) ≫
        Iso.inv
          (pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))
            (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))
      (fst
        (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
        (Spec.map
          (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (CommRingCat.of (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))) (Y :=
        Spec (CommRingCat.of (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))) (Z :=
        Spec (CommRingCat.of ↥(𝒜 0)))
        (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
        (Spec.map
          (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))))
      (Spec.map (CommRingCat.ofHom F) ≫
        Iso.inv
          (pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))
            (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))
      (fst
        (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
        (Spec.map
          (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))))
have h : Iso.inv (pullbackAwayιIso 𝒜 sorry sorry sorry sorry sorry) ≫
    CategoryStruct.comp (Y :=
      pullback (X := Proj 𝒜) (Y :=
        pullback (X := Spec (AffineCover.X (P := IsOpenImmersion) (affineOpenCover 𝒜) i)) (Y :=
          Spec (AffineCover.X (P := IsOpenImmersion) (affineOpenCover 𝒜) j))
          (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry ≫ toSpecZero 𝒜)
          (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry ≫ toSpecZero 𝒜))
        (Z := diagonalObj (X := Proj 𝒜) (toSpecZero 𝒜)) (diagonal (toSpecZero 𝒜))
        (pullback.map (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry ≫ toSpecZero 𝒜)
          (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry ≫ toSpecZero 𝒜) (toSpecZero 𝒜) (toSpecZero 𝒜)
          (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry)
          (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry) (𝟙 (Spec (CommRingCat.of ↥(𝒜 0)))) sorry sorry))
      (Iso.inv
        (pullbackDiagonalMapIdIso (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry)
          (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry) (toSpecZero 𝒜)))
      (snd (diagonal (toSpecZero 𝒜))
          (pullback.map (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry ≫ toSpecZero 𝒜)
            (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry ≫ toSpecZero 𝒜) (toSpecZero 𝒜)
            (toSpecZero 𝒜) (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry)
            (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry) (𝟙 (Spec (CommRingCat.of ↥(𝒜 0)))) sorry sorry) ≫
        fst (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i ≫ toSpecZero 𝒜)
          (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j ≫ toSpecZero 𝒜)) =
  Spec.map
    (CategoryStruct.comp (Y :=
      CommRingCat.of
        (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
          Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
      (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom) (CommRingCat.ofHom F))
Tactic: simp only [Iso.trans_hom, congrHom_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id,
      limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, e₂, e₁,
      pullbackSpecIso_inv_fst, ← Spec.map_comp]