-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
this :
  X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        r) =
    (↑U : X.Opens)
⊢ P (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
    (↑Γ(X,
          X.basicOpen (U := (↑U : X.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                  (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
              r)) :
      Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))) : Type u) (P := (↑Γ(X, (↑U : X.Opens)) : Type u))
          (↑(X.presheaf.1
                (op
                  (X.basicOpen (U := (↑U : X.Opens))
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                          (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
                        (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
                      r)))) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯)) r)))
have to_basicOpen : P (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
  (↑Γ(X,
        X.basicOpen (U := (↑U : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
            r)) :
    Type u))
  (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))) : Type u) (P := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (↑(X.presheaf.1
          (op
            (X.basicOpen (U := (↑U : X.Opens))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                    (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
                r)))) :
      Type u)
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry)) r)
Tactic: simp only [CommRingCat.hom_ofHom]