-- 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 𝒜)))
⊢ IsClosedImmersion (X :=
    PreZeroHypercover.X (S := Proj 𝒜)
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (T := diagonalObj (X := Proj 𝒜) (toSpecZero 𝒜)) (diagonal (toSpecZero 𝒜))
          (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
            (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜))))
      (i, j))
    (Cover.pullbackHom (P := IsOpenImmersion)
        (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
          (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜))
        (diagonal (toSpecZero 𝒜)) (i, j) :
      PreZeroHypercover.X (S := Proj 𝒜)
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (T := diagonalObj (X := Proj 𝒜) (toSpecZero 𝒜))
              (diagonal (toSpecZero 𝒜))
              (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
                (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜))))
          (i, j) ⟶
        PreZeroHypercover.X (S := diagonalObj (X := Proj 𝒜) (toSpecZero 𝒜))
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
              (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜)))
          (i, j))
have dsimp : IsClosedImmersion (X :=
  pullback (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))
  (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))
Tactic: dsimp [Scheme, Cover.pullbackHom]