-- 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))ᵒᵖ
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 ⋯))))
    (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))))
    (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 ⋯)))

Tactic:
simp_rw [← Γ_map_op]

Premises used: AlgebraicGeometry.LocallyRingedSpace.Γ_map_op