-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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)
⊢ 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
have 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)))
Tactic: simp [hU.app_basicOpen_eq_away_map f h]