-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
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))
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) ⋯) :
                          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
                        (↑r : (↑Γ(Y, ⊤) : Type u))))
                    ⋯) :
                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) ⋯) :
                        (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
                      (↑r : (↑Γ(Y, ⊤) : Type u))))
                  ⋯) :
              X.Opens)
            ⋯))),
    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)))
⊢ 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)))

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])