-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
f :
  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 r)) ⟶
    X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst :
  IsLocalization.Away r
    (↑(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 r))) :
      Type u)
mp :
  Eq (α :=
      (↑(CommRingCat.of (↑(Γ.obj (op X)) : Type u)) : Type u) →+*
        (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (X := CommRingCat.of (↑(Γ.obj (op X)) : 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)))
                  (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
                (op (basicOpen r)))) ≫
          f))
      (@RingHom.comp _
        (↑(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 r))) :
          Type u)
        _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.lift r ⋯)
        (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 r))) :
            Type u))) →
    f = X.toΓSpecCApp r
⊢ Eq (α :=
      (↑(CommRingCat.of (↑(Γ.obj (op X)) : Type u)) : Type u) →+*
        (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (X := CommRingCat.of (↑(Γ.obj (op X)) : 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)))
                  (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
                (op (basicOpen r)))) ≫
          f))
      (@RingHom.comp _
        (↑(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 r))) :
          Type u)
        _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.lift r ⋯)
        (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 r))) :
            Type u))) ↔
    f = X.toΓSpecCApp r
have mpr : f = X.toΓSpecCApp r →
  Eq (α :=
    (↑(CommRingCat.of (↑(Γ.obj (op X)) : Type u)) : Type u) →+*
      (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) (X := CommRingCat.of (↑(Γ.obj (op X)) : 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)))
                (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r)))) ≫
        f))
    (@RingHom.comp _
      (↑(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 r))) :
        Type u)
      _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.lift r sorry)
      (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 r))) :
          Type u)))
Tactic: constructor