-- 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 (↑(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 ⋯)))
have simp_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 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 sorry))))
  (f.unop ≫ X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: simp_rw [← Γ_map_op]