-- 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))
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)
        ⋯))
of_basicOpenCover :
  ∀
    (this :
      P (R := (↑Γ(Y, Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Type u)) (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
          (CommRingCat.ofHom
            (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))))) : 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 : (↑Γ(Y, ⊤) : Type u)))))) :
                Type u)
              (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)))
of_basicOpenCover₁ :
  ∀
    (this :
      P (R := (↑Γ(Y, Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Type u)) (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))
        (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))))) : 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 : (↑Γ(Y, ⊤) : Type u)))))) :
            Type u)
          (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)))
of_basicOpenCover₂ of_basicOpenCover₃ of_basicOpenCover₄ of_basicOpenCover₅ :
  ∀
    (this :
      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)))
⊢ 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:
rwa [IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2, CommRingCat.hom_ofHom,
      ← h₁.isLocalization_away_iff] at this

Premises used: AlgebraicGeometry.isAffineOpen_top, CommRingCat.hom_ofHom, RingHom.RespectsIso.isLocalization_away_iff, Subtype.property, AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map