-- 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) ⟶
      (forgetToSheafedSpace.obj X).presheaf.obj ((Opens.map (forgetToSheafedSpace.map β).hom.base).op.obj (op U)))
    ((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))) ≫
        (forgetToSheafedSpace.map (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).hom.c.app (op U)) ≫
      (forgetToSheafedSpace.obj 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))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U))
have erw : Eq (α :=
  CommRingCat.of (↑R : Type u) ⟶
    (forgetToSheafedSpace.obj X).presheaf.obj ((Opens.map (forgetToSheafedSpace.map β).hom.base).op.obj (op U)))
  (CategoryStruct.comp (Y :=
    (Functor.obj
          (pushforward CommRingCat (forgetToSheafedSpace.map (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).hom.base)
          (forgetToSheafedSpace.obj X).presheaf).obj
      (op U))
    (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
        CategoryStruct.comp (Y :=
          CommRingCat.of
            (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf
                      (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                    (structureSheaf (↑(Γ.obj (op X)) : Type u)))
                  (op
                    ((Opens.comap
                          { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := sorry :
                            C(PrimeSpectrum (↑(Γ.obj (op X)) : Type u), PrimeSpectrum (↑R : Type u)) } :
                        (a : Opens (PrimeSpectrum (↑R : Type u))) → Opens (PrimeSpectrum (↑(Γ.obj (op X)) : Type u)))
                      U))) :
              Type u))
          (CommRingCat.ofHom
            (algebraMap (↑(Γ.obj (op X)) : Type u)
              (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
                    (ObjectProperty.FullSubcategory.obj (P :=
                      Presheaf.IsSheaf
                        (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                      (structureSheaf (↑(Γ.obj (op X)) : Type u)))
                    (op
                      ((Opens.comap
                            { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := sorry :
                              C(PrimeSpectrum (↑(Γ.obj (op X)) : Type u), PrimeSpectrum (↑R : Type u)) } :
                          (a : Opens (PrimeSpectrum (↑R : Type u))) → Opens (PrimeSpectrum (↑(Γ.obj (op X)) : Type u)))
                        U))) :
                Type u)))
          ({ hom := X.toΓSpecSheafedSpace.hom }.hom.c.app
            (op
              ((Opens.map
                    { hom := (Spec.sheafedSpaceMap f).hom :
                          InducedCategory.Hom (D := PresheafedSpace CommRingCat) (F := SheafedSpace.toPresheafedSpace)
                            (Spec.locallyRingedSpaceObj (Γ.obj (op X))).toSheafedSpace
                            (Spec.sheafedSpaceObj R) }.hom.base).obj
                (unop (op U))))) :
      CommRingCat.of (↑R : Type u) ⟶
        (Functor.obj
              (pushforward CommRingCat (forgetToSheafedSpace.map (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).hom.base)
              (forgetToSheafedSpace.obj X).presheaf).obj
          (op U))
    ((forgetToSheafedSpace.obj X).presheaf.map (eqToHom sorry) :
      (forgetToSheafedSpace.obj X).presheaf.obj
          ((Opens.map (forgetToSheafedSpace.map (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).hom.base).op.obj (op U)) ⟶
        (forgetToSheafedSpace.obj X).presheaf.obj ((Opens.map (forgetToSheafedSpace.map β).hom.base).op.obj (op U))))
  (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))) ≫
    (forgetToSheafedSpace.map β).hom.c.app (op U))
Tactic: erw [SheafedSpace.comp_hom_c_app, toOpen_comp_comap_assoc]