-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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))ᵒᵖ
⊢ 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 ⋯)))
have 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 sorry))))
  (f.unop ≫ X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
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']