-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf_1 :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
this : IsAffine X
a : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
left : IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme)
hf :
  Q (R := (↑Γ((↑(Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))).ι ''ᵁ ⊤)))
refine_2 :
  ∀
    (hf :
      Q (R := (↑Γ(Y, (Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))).ι ''ᵁ ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))).ι ''ᵁ ⊤)))),
    Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)) (S :=
      (↑Γ(X,
            X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Scheme.Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑a : (↑Γ(Y, ⊤) : Type u)))) :
        Type u))
      (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)
        (↑Γ(X,
              X.basicOpen (U := ⊤)
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (Scheme.Hom.appTop f) :
                    (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                  (↑a : (↑Γ(Y, ⊤) : Type u)))) :
          Type u)
        (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))
⊢ Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)) (S :=
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              (↑a : (↑Γ(Y, ⊤) : Type u)))) :
      Type u))
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)
      (↑Γ(X,
            X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Scheme.Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑a : (↑Γ(Y, ⊤) : Type u)))) :
        Type u)
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))

Tactic:
have hf : Q (Scheme.Hom.app f ((Y.basicOpen a.1).ι ''ᵁ ⊤)).hom := hf