-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : (↑Γ(Y, U) : Type u)
this_1 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u) := ⋯
this : IsLocalization.Away (R := (↑Γ(X, V) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
      r :
    (↑Γ(X, V) : Type u))
  (↑Γ(X,
        X.basicOpen (U := V)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
              (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
            r)) :
    Type u) :=
  ⋯
⊢ CommRingCat.Hom.hom
      (Scheme.Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := V)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
              (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
            r))
        ⋯) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))) : Type u)
          (↑(X.presheaf.1
                (op
                  (X.basicOpen (U := V)
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
                        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
                      r)))) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r))
have hf : Eq (α :=
  (↑Γ(Y, U) : Type u) →+*
    (↑Γ(X,
          X.basicOpen (U := V)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
              r)) :
      Type u))
  ((CommRingCat.Hom.hom
        (Scheme.Hom.appLE f (Y.basicOpen r)
          (X.basicOpen (U := V)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
              r))
          sorry)).comp
    (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))
  (RingHom.comp (β := (↑Γ(Y, Y.basicOpen r) : Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))) : Type u)
          (↑(X.presheaf.1
                (op
                  (X.basicOpen (U := V)
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
                        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
                      r)))) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r)))
    (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))
Tactic: apply IsLocalization.ringHom_ext (.powers r)