-- 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 :=
    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) ⋯ ⋯ ≫ 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)))) ⋯ ⋯))
    (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)))) ⋯ ⋯))
have refine : IsClosedImmersion (X :=
  pullback (X := Spec (AffineCover.X (P := IsOpenImmersion) (affineOpenCover 𝒜) i))
    (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry)
    (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry))
  (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 𝒜))
  (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)))
Tactic: refine (MorphismProperty.cancel_left_of_respectsIso (P := @IsClosedImmersion)
    (f := (pullbackDiagonalMapIdIso ..).inv) _).mp ?_