-- 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)))
⊢ 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 =
    Spec.map (CommRingCat.ofHom F)
have h : Eq (α :=
  Spec
      (CommRingCat.of
        (Away 𝒜
          ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))) ⟶
    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) 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)) ≫
        e₁.hom) ≫
    Iso.inv
      (pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))
        (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))))
Tactic: rw [← cancel_mono (pullbackSpecIso ..).inv]