-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
r_1 : (↑(Γ.obj (op X)) : Type u)
r s : (InducedCategory (C := (↑(Γ.obj (op X)) : Type u)) (Opens (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))) basicOpen)ᵒᵖ
f : r ⟶ s
h :
  (CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
        Functor.obj
          (Functor.op (inducedFunctor basicOpen) ⋙
            (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
          s) =
      (CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen (unop s)))) →
    Eq (α :=
      CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
        Functor.obj
          (Functor.op (inducedFunctor basicOpen) ⋙
            (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
          s)
      (CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.op (inducedFunctor basicOpen) ⋙
            (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
          r)
        (X.toToΓSpecMapBasicOpen (unop r))
        (CategoryTheory.Functor.map
          (Functor.op (inducedFunctor basicOpen) ⋙
            (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
          f))
      (X.toToΓSpecMapBasicOpen (unop s))
⊢ Eq (α :=
    CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        s)
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
            (structureSheaf (↑(Γ.obj (op X)) : Type u)))
        s)
      (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)) : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen (unop r))))) ≫
        CategoryTheory.Functor.map
          (Functor.op (inducedFunctor basicOpen) ⋙
            ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
              (structureSheaf (↑(Γ.obj (op X)) : Type u)))
          f)
      (X.toΓSpecCApp (unop s)))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        r)
      (X.toToΓSpecMapBasicOpen (unop r))
      (CategoryTheory.Functor.map
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        f))

Tactic:
convert! X.toΓSpecCApp_spec s.unop

Premises used: AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, Opposite.unop