-- 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_2 :
  Q (R := (↑Γ((↑(Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))).ι ''ᵁ ⊤)))
hf :
  Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
          (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)
            (↑Γ(X,
                  X.basicOpen (U := f ⁻¹ᵁ ⊤)
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
                        (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                      (↑a : (↑Γ(Y, ⊤) : Type u)))) :
              Type u)
            (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)) (↑a : (↑Γ(Y, ⊤) : Type u))) ≫
        X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))))
refine_2 :
  ∀
    (hf :
      Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u))
        ((CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))).comp
          (CommRingCat.Hom.hom
            (CommRingCat.ofHom
              (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)
                (↑Γ(X,
                      X.basicOpen (U := f ⁻¹ᵁ ⊤)
                        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                              (CC := CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
                            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                          (↑a : (↑Γ(Y, ⊤) : Type u)))) :
                  Type u)
                (CommRingCat.Hom.hom (Scheme.Hom.app 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)))
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  ∀
    (hf :
      Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)) (S :=
        (↑(CommRingCat.of
              (↑Γ(X,
                    X.basicOpen (U := f ⁻¹ᵁ ⊤)
                      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
                          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                        (↑a : (↑Γ(Y, ⊤) : Type u)))) :
                Type u)) :
          Type u))
        (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)
              (↑Γ(X,
                    X.basicOpen (U := f ⁻¹ᵁ ⊤)
                      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
                          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                        (↑a : (↑Γ(Y, ⊤) : Type u)))) :
                Type u)
              (CommRingCat.Hom.hom (Scheme.Hom.app 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)))
⊢ 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:
rwa [CommRingCat.hom_comp, hPi.cancel_right_isIso] at hf

Premises used: RingHom.RespectsIso.cancel_right_isIso, CommRingCat.hom_comp