-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)
r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)
ha :
  IsAffineOpen
    (X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r'))
hxa :
  x ∈
    X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r')
s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)
s' :
  (↑Γ(X,
        X.basicOpen (U := (↑V₂ : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
              (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
            r')) :
    Type u)
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this_1 :
  IsLocalization.Away (R := (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r' :
      (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
    (↑Γ(X,
          X.basicOpen (U := (↑V₂ : X.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
                (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
              r')) :
      Type u)
this_2 : IsLocalization.Away r' (↑Γ(Y, Y.basicOpen r') : Type u)
this : IsLocalization.Away s' (↑Γ(X, X.basicOpen s') : Type u)
ers : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
heq :
  Eq (α := Γ(Y, Y.basicOpen r') ⟶ Γ(X, X.basicOpen s')) (Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen s') ⋯)
    (Scheme.Hom.appLE f (Y.basicOpen r')
        (X.basicOpen (U := (↑V₂ : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
              (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
            r'))
        ⋯ ≫
      CommRingCat.ofHom
        (algebraMap
          (↑(X.presheaf.1
                (Opposite.op
                  (X.basicOpen (U := (↑V₂ : X.Opens))
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
                        (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
                      r')))) :
            Type u)
          (↑(X.presheaf.1 (Opposite.op (X.basicOpen s'))) : Type u)))
rw :
  P (S := (↑Γ(X, X.basicOpen s') : Type u))
    (CommRingCat.Hom.hom
      (Scheme.Hom.appLE f (Y.basicOpen r')
          (X.basicOpen (U := (↑V₂ : X.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
                (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
              r'))
          ⋯ ≫
        CommRingCat.ofHom
          (algebraMap
            (↑(X.presheaf.1
                  (Opposite.op
                    (X.basicOpen (U := (↑V₂ : X.Opens))
                      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
                          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
                        r')))) :
              Type u)
            (↑(X.presheaf.1 (Opposite.op (X.basicOpen s'))) : Type u))))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) ers))

Tactic:
rw [f.appLE_congr _ hBrr' hBss' (fun f => P f.hom), heq]

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.Scheme.Hom.appLE_congr