-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f_1 : A →+* (↑Γ(X, ⊤) : Type u)
x_1 x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
x y : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
e : pullback ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≅
  (↑(X.basicOpen (U := ⊤)
        ((f : (a : A) → (↑Γ(X, ⊤) : Type u))
          (x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
              0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i))) *
            y.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
              0 < y.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                r ∈ 𝒜 (y.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))) :
    Scheme) :=
  Iso.symm (IsPullback.isoPullback ⋯) ≪≫ X.isoOfEq ⋯
rw :
  Eq (α :=
    (↑(X.basicOpen (U := ⊤)
            ((f : (a : A) → (↑Γ(X, ⊤) : Type u))
              (x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
                  0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                    r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i))) *
                y.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
                  0 < y.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                    r ∈ 𝒜 (y.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))) :
        Scheme) ⟶
      Proj 𝒜)
    (e.inv ≫
      pullback.fst ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≫
        (fun (ri : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀) ↦
            (toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫
                Scheme.Opens.ι
                  (basicOpen 𝒜
                    (ri.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
                      0 < ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                        r ∈ 𝒜 (ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i))))) :
              (openCoverOfMapIrrelevantEqTop 𝒜 f hf).X ri ⟶ Proj 𝒜))
          x)
    (e.inv ≫
      pullback.snd ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≫
        (fun (ri : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀) ↦
            (toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫
                Scheme.Opens.ι
                  (basicOpen 𝒜
                    (ri.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
                      0 < ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                        r ∈ 𝒜 (ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i))))) :
              (openCoverOfMapIrrelevantEqTop 𝒜 f hf).X ri ⟶ Proj 𝒜))
          y)
⊢ Eq (α := pullback ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ⟶ Proj 𝒜)
    (pullback.fst ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≫
      (fun (ri : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀) ↦
          (toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫
              Scheme.Opens.ι
                (basicOpen 𝒜
                  (ri.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
                    0 < ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                      r ∈ 𝒜 (ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i))))) :
            (openCoverOfMapIrrelevantEqTop 𝒜 f hf).X ri ⟶ Proj 𝒜))
        x)
    (pullback.snd ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≫
      (fun (ri : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀) ↦
          (toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫
              Scheme.Opens.ι
                (basicOpen 𝒜
                  (ri.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
                    0 < ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
                      r ∈ 𝒜 (ri.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i))))) :
            (openCoverOfMapIrrelevantEqTop 𝒜 f hf).X ri ⟶ Proj 𝒜))
        y)

Tactic:
rw [← cancel_epi e.inv]

Premises used: CategoryTheory.cancel_epi, CategoryTheory.Iso.inv