-- 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 : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
e_a :
  Eq (α :=
    ↥(𝒜 0) →+*
      Localization.Away (M := (↑Γ(X, ⊤) : Type 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)))) :
          (↑Γ(X, ⊤) : Type u)))
    (@RingHom.comp _
      (Localization.Away
        (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)))))
      _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map
        (Localization.Away (M := (↑Γ(X, ⊤) : Type 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)))) :
            (↑Γ(X, ⊤) : Type u)))
        f ⋯)
      (@RingHom.comp _
        (HomogeneousLocalization 𝒜
          (Submonoid.powers
            (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))))))
        _ _ Semiring.toNonAssocSemiring _
        (algebraMap
          (Away 𝒜
            (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)))))
          (Localization.Away
            (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))))))
        (algebraMap (↥(𝒜 0))
          (HomogeneousLocalization 𝒜
            (Submonoid.powers
              (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)))))))))
    (RingHom.comp
      (algebraMap (↑Γ(X, ⊤) : Type u)
        (Localization.Away (M := (↑Γ(X, ⊤) : Type 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)))) :
            (↑Γ(X, ⊤) : Type u))))
      (f.comp (algebraMap (↥(𝒜 0)) A)))
⊢ Eq (α :=
    ↥(𝒜 0) →+*
      Localization.Away (M := (↑Γ(X, ⊤) : Type 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)))) :
          (↑Γ(X, ⊤) : Type u)))
    (@RingHom.comp _
      (HomogeneousLocalization 𝒜
        (Submonoid.powers
          (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))))))
      _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _
        (Localization.Away
          (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)))))
        _ _ Semiring.toNonAssocSemiring _
        (IsLocalization.map
          (Localization.Away (M := (↑Γ(X, ⊤) : Type 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)))) :
              (↑Γ(X, ⊤) : Type u)))
          f ⋯)
        (algebraMap
          (Away 𝒜
            (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)))))
          (Localization.Away
            (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)))))))
      (algebraMap (↥(𝒜 0))
        (HomogeneousLocalization 𝒜
          (Submonoid.powers
            (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))))))))
    (RingHom.comp
      (algebraMap (↑Γ(X, ⊤) : Type u)
        (Localization.Away (M := (↑Γ(X, ⊤) : Type 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)))) :
            (↑Γ(X, ⊤) : Type u))))
      (f.comp (algebraMap (↥(𝒜 0)) A)))
have e_a₁ : Eq (α :=
  ↥(𝒜 0) →+*
    Localization.Away (M := (↑Γ(X, ⊤) : Type 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)))) :
        (↑Γ(X, ⊤) : Type u)))
  (@RingHom.comp _
    (Localization.Away
      (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)))))
    _ _ Semiring.toNonAssocSemiring _
    (IsLocalization.map
      (Localization.Away (M := (↑Γ(X, ⊤) : Type 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)))) :
          (↑Γ(X, ⊤) : Type u)))
      f sorry)
    (algebraMap (↥(𝒜 0))
      (Localization.Away
        (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)))))))
  (RingHom.comp
    (algebraMap (↑Γ(X, ⊤) : Type u)
      (Localization.Away (M := (↑Γ(X, ⊤) : Type 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)))) :
          (↑Γ(X, ⊤) : Type u))))
    (f.comp (algebraMap (↥(𝒜 0)) A)))
Tactic: rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq _ A,
    ← RingHom.comp_assoc, IsLocalization.map_comp, RingHom.comp_assoc]