-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
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 𝒜)))
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) ⋯ ⋯ ≫ 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)))) ⋯ ⋯))
⊢ 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))

Tactic:
dsimp [Scheme, Cover.pullbackHom]

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, AlgebraicGeometry.Scheme