-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
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 ⋯
⊢ 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)
have 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 sorry sorry sorry ≫
              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 sorry sorry sorry ≫
              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]