-- Module: Mathlib.AlgebraicGeometry.AffineScheme
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) :=
  ⋯
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))
            ⋯)).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)))
⊢ 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))

Tactic:
apply IsLocalization.ringHom_ext (.powers r)

Premises used: Submonoid.powers, IsLocalization.ringHom_ext