-- 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 𝒜)))
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)))
h :
  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))))
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 ⋯ ⋯)))
    (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)))
⊢ 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 (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i)
        (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j))
      (Iso.inv (pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯))
      (fst (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯)
        (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯)))
    (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:
erw [pullbackAwayιIso_inv_fst]

Premises used: AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst