-- 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) :=
  ⋯
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.map
            (↑(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)) ⋯)))
      (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen 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) _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map
        (↑(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)) ⋯)
      (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))
hf₂ :
  (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
      (algebraMap (↑Γ(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 U V e))
⊢ 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)))
have hf₃ : (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
    (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE sorry).op)) =
  RingHom.comp
    (algebraMap (↑Γ(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 U V e))
Tactic: rw [IsLocalization.Away.map, CommRingCat.hom_ofHom, IsLocalization.map_comp,
    RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
    ← CommRingCat.hom_comp, Scheme.Hom.appLE_map, Scheme.Hom.map_appLE]