-- 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))))
    (Quiver.Hom.unop (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))) ≫
      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 ⊤))
        (Γ.map
          (Quiver.Hom.op
            ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
                (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                  X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
              f)))
        (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 ⋯)))
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
      (Γ.rightOp.map
          ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R)) :
              (a : op (X.presheaf.obj (op ⊤)) ⟶ op (CommRingCat.of R)) →
                X ⟶ Spec.locallyRingedSpaceObj (CommRingCat.of R))
            f) ≫
        locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))) ≫
    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 [← Γ.rightOp_map_unop, ← Category.assoc, ← unop_comp]