-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
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 := ⋯ :
                              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 := ⋯ :
                                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 ⋯) :
        (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))
⊢ 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))

Tactic:
erw [SheafedSpace.comp_hom_c_app, toOpen_comp_comap_assoc]

Premises used: AlgebraicGeometry.SheafedSpace.comp_hom_c_app, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc