-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X_1 Y_1 : Scheme
U_1 : X_1.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X_1, U_1) : Type u)
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
simp :
  Eq (α :=
    Γ(Y, Y.basicOpen r) ⟶
      CommRingCat.of
        (↑Γ(X,
              X.basicOpen (U := f ⁻¹ᵁ U)
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (Scheme.Hom.app f U) :
                    (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                  r)) :
          Type u))
    (CommRingCat.ofHom
      (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
        (↑Γ(X,
              X.basicOpen (U := f ⁻¹ᵁ U)
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (Scheme.Hom.app f U) :
                    (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                  r)) :
          Type u)
        (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r))
    (CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ U)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.app f U) :
                      (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                    r)) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      𝟙
        Γ(X,
          X.basicOpen (U := f ⁻¹ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.app f U) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
              r)))
⊢ Iso.hom (Iso.refl (Arrow.mk (X := Γ(Y, Y.basicOpen r)) (Scheme.Hom.app f (Y.basicOpen r))).left) ≫
      (Arrow.mk (X := CommRingCat.of (↑Γ(Y, Y.basicOpen r) : Type u)) (Y :=
          CommRingCat.of
            (↑Γ(X,
                  X.basicOpen (U := f ⁻¹ᵁ U)
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (Scheme.Hom.app f U) :
                        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                      r)) :
              Type u))
          (CommRingCat.ofHom
            (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
              (↑Γ(X,
                    X.basicOpen (U := f ⁻¹ᵁ U)
                      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := CommRingCat.carrier) (Scheme.Hom.app f U) :
                          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                        r)) :
                Type u)
              (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r))).hom =
    (Arrow.mk (X := Γ(Y, Y.basicOpen r)) (Scheme.Hom.app f (Y.basicOpen r))).hom ≫
      (Functor.mapIso X.presheaf (Iso.op (eqToIso ⋯))).hom

Tactic:
simp [hU.app_basicOpen_eq_away_map f h]

Premises used: AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map