-- 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)))
⊢ 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₁ : 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) _ _ 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)) sorry)
    (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))
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]