-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : (↑R : Type u)),
    Eq (α := R ⟶ X.presheaf.obj (op ((Opens.map β.base).obj (basicOpen r))))
      (f ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (CommRingCat.ofHom
          (algebraMap (↑R : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (structureSheafInType (↑R : Type u) (↑R : Type u)))
              (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r)))
r : (↑R : Type u)
U : Opens (PrimeSpectrum (↑R : Type u)) := basicOpen r
⊢ Eq (α := CommRingCat.of (↑R : Type u) ⟶ X.presheaf.obj (op ((Opens.map β.base).obj U)))
    (CategoryStruct.comp (Y := X.presheaf.obj (op ((Opens.map X.toΓSpecBase).obj ((Opens.map (Spec.topMap f)).obj U))))
      (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
        CommRingCat.ofHom
            (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u)
              (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(X.presheaf.obj (op ⊤)) : Type u)) : Type u))ᵒᵖ)
                    (ObjectProperty.FullSubcategory.obj (P :=
                      Presheaf.IsSheaf
                        (Opens.grothendieckTopology
                          (↑(PrimeSpectrum.Top (↑(X.presheaf.obj (op ⊤)) : Type u)) : Type u)))
                      (structureSheaf (↑(X.presheaf.obj (op ⊤)) : Type u)))
                    (op
                      ((Opens.comap
                            { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ :
                              C(PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u), PrimeSpectrum (↑R : Type u)) } :
                          (a : Opens (PrimeSpectrum (↑R : Type u))) →
                            Opens (PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u)))
                        U))) :
                Type u)) ≫
          X.toΓSpecSheafedSpace.hom.c.app (op ((Opens.map (Spec.topMap f)).obj U)))
      (X.presheaf.map (eqToHom ⋯)))
    (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheafInType (↑R : Type u) (↑R : Type u)))
            (op U))) ≫
      β.c.app (op U))
have rw : Eq (α := CommRingCat.of (↑R : Type u) ⟶ X.presheaf.obj (op ((Opens.map β.base).obj U)))
  (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
    CategoryStruct.comp (Y := X.presheaf.obj (op ((Opens.map X.toΓSpecBase).obj ((Opens.map (Spec.topMap f)).obj U))))
      (CommRingCat.ofHom
          (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u)
            (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(X.presheaf.obj (op ⊤)) : Type u)) : Type u))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf
                      (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(X.presheaf.obj (op ⊤)) : Type u)) : Type u)))
                    (structureSheaf (↑(X.presheaf.obj (op ⊤)) : Type u)))
                  (op
                    ((Opens.comap
                          { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := sorry :
                            C(PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u), PrimeSpectrum (↑R : Type u)) } :
                        (a : Opens (PrimeSpectrum (↑R : Type u))) →
                          Opens (PrimeSpectrum (↑(X.presheaf.obj (op ⊤)) : Type u)))
                      U))) :
              Type u)) ≫
        X.toΓSpecSheafedSpace.hom.c.app (op ((Opens.map (Spec.topMap f)).obj U)))
      (X.presheaf.map (eqToHom sorry)))
  (CommRingCat.ofHom
      (algebraMap (↑R : Type u)
        (Functor.obj
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheafInType (↑R : Type u) (↑R : Type u)))
          (op U))) ≫
    β.c.app (op U))
Tactic: rw [Category.assoc]