-- 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.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))
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
      (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).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))
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
      (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)) =
    RingHom.comp (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))
hf₅ :
  CommRingCat.Hom.hom
      (Y.presheaf.map (homOfLE ⋯).op ≫
        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))
          ⋯) =
    RingHom.comp (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))
hf₆ :
  CommRingCat.Hom.hom
      (Y.presheaf.map (homOfLE ⋯).op ≫
        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 (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
hf₇ :
  CommRingCat.Hom.hom
      (Y.presheaf.map (homOfLE ⋯).op ≫
        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
      (Scheme.Hom.appLE f U
        (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))
        ⋯)
hf₈ hf₉ :
  CommRingCat.Hom.hom
      (Scheme.Hom.appLE f U
        (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
      (Scheme.Hom.appLE f U
        (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))
        ⋯)
⊢ 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)))

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]

Premises used: IsLocalization.map_comp, CommRingCat.hom_comp, IsLocalization.Away.map, CommRingCat.hom_ofHom, RingHom.algebraMap_toAlgebra, AlgebraicGeometry.Scheme.Hom.map_appLE, AlgebraicGeometry.Scheme.Hom.appLE_map