-- 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
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
U : (↑X.affineOpens : Type u)
r : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
hs' :
  ∀ (r : ↥s) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) (↑V : X.Opens) e))
⊢ P (S :=
    Localization.Away (M := (↑Γ(X, (↑U : X.Opens)) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)) :
        (↑Γ(X, (↑U : X.Opens)) : Type u)))
    (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯)) (↑r : (↑Γ(Y, ⊤) : Type u)))
have of_basicOpenCover : ∀
  (this :
    P (S :=
      (↑Γ(X,
            (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
                  (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 : (↑Γ(Y, ⊤) : Type u))))
                  sorry) :
              X.Opens)) :
        Type u))
      (CommRingCat.Hom.hom
        (Scheme.Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
                (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 : (↑Γ(Y, ⊤) : Type u))))
                sorry) :
            X.Opens)
          sorry))),
  P (S :=
    Localization.Away (M := (↑Γ(X, (↑U : X.Opens)) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)) :
        (↑Γ(X, (↑U : X.Opens)) : Type u)))
    (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry)) (↑r : (↑Γ(Y, ⊤) : Type u)))
Tactic: have := hs' r ⟨X.basicOpen (f.appLE ⊤ U le_top r.1), U.2.basicOpen (f.appLE ⊤ U le_top r.1)⟩
      (by simp [Scheme.Hom.appLE])