-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
R : Type u
inst : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens (↑(↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace : TopCat) : Type u))ᵒᵖ
rw :
  Eq (α :=
    CommRingCat.of R ⟶
      X.presheaf.obj
        (op
          (Functor.obj
            (Opens.map
              (PresheafedSpace.Hom.base
                (Hom.toHom
                  ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                      (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                        X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
                    f))))
            (unop U))))
    (Quiver.Hom.unop
        (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of (↑(unop (op (CommRingCat.of R))) : Type u)))) ≫
      CategoryStruct.comp (Y :=
        Functor.obj (C :=
          (Opens (↑(↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace : TopCat) : Type u))ᵒᵖ)
          (Functor.obj
            (pushforward CommRingCat
              (PresheafedSpace.Hom.base
                (Hom.toHom
                  ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                      (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                        X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
                    f))))
            X.presheaf)
          (op ⊤))
        (NatTrans.app
          (PresheafedSpace.Hom.c
            (Hom.toHom
              ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                  (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                    X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
                f)))
          (op ⊤))
        (CategoryTheory.Functor.map
          (Functor.obj
            (pushforward CommRingCat
              (PresheafedSpace.Hom.base
                (Hom.toHom
                  ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                      (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                        X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
                    f))))
            X.presheaf)
          (Quiver.Hom.op (homOfLE ⋯))))
    (f.unop ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ Eq (α :=
    CommRingCat.of R ⟶
      X.presheaf.obj
        (op
          (Functor.obj
            (Opens.map
              (PresheafedSpace.Hom.base
                (Hom.toHom
                  ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                      (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                        X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
                    f))))
            (unop U))))
    (CommRingCat.ofHom
        (algebraMap R
          (Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R R))
            U)) ≫
      NatTrans.app
        (PresheafedSpace.Hom.c
          (Hom.toHom
            ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                  X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
              f)))
        U)
    (f.unop ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
rw [← StructureSheaf.algebraMap_self_map _ U _ (homOfLE le_top).op, Category.assoc,
    NatTrans.naturality _ (homOfLE (le_top (a := U.unop))).op,
    ← unop_locallyRingedSpaceAdjunction_counit_app']

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.op, AlgebraicGeometry.StructureSheaf.algebraMap_self_map, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', le_top, CategoryTheory.NatTrans.naturality, CategoryTheory.homOfLE