-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
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
⊢ Eq (α :=
    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)))
        r ⟶
      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)
    (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))
    (X.toΓSpecCApp (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)
have a : 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 :=
    CommRingCat.of
      (↑(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)))
              (structureSheaf (↑(Γ.obj (op X)) : Type u)))
            (op (basicOpen (unop r)))) :
        Type u))
    (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)))
                  (structureSheaf (↑(Γ.obj (op X)) : Type u)))
                (op (basicOpen (unop r)))) :
            Type u)) :
      CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
        CommRingCat.of
          (↑(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)))
                  (structureSheaf (↑(Γ.obj (op X)) : Type u)))
                (op (basicOpen (unop r)))) :
            Type u))
    (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) :
      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)))
          r ⟶
        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 :=
    CommRingCat.of
      (↑(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)))
              (structureSheaf (↑(Γ.obj (op X)) : Type u)))
            (op (basicOpen (unop r)))) :
        Type u))
    (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)))
                (structureSheaf (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen (unop r)))) :
          Type u)))
    (X.toΓSpecCApp (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: apply (StructureSheaf.to_basicOpen_epi (Γ.obj (op X)) r.unop).1