-- 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
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)
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) ⋯) :
                (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) ⋯) :
                    (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
                  r)))) :
        Type u)
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯)) r)
⊢ 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)))

Tactic:
simp only [CommRingCat.hom_ofHom]

Premises used: CommRingCat.hom_ofHom