Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this✝¹ :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
this✝ : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
this : IsLocalization.Away s' ↑Γ(X, X.basicOpen s')
ers : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
heq :
  Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen s') ⋯ =
    Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
        ⋯ ≫
      CommRingCat.ofHom
        (algebraMap
          ↑(X.presheaf.1 (Opposite.op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))))
          ↑(X.presheaf.1 (Opposite.op (X.basicOpen s'))))
⊢ P
    (Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
        ⋯).hom'

Tactic:
rw [U₂.2.appLE_eq_away_map f V₂.2]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this✝¹ :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
this✝ : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
this : IsLocalization.Away s' ↑Γ(X, X.basicOpen s')
ers : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
heq :
  Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen s') ⋯ =
    Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
        ⋯ ≫
      CommRingCat.ofHom
        (algebraMap
          ↑(X.presheaf.1 (Opposite.op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))))
          ↑(X.presheaf.1 (Opposite.op (X.basicOpen s'))))
⊢ P
    (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.1 (Opposite.op (Y.basicOpen r'))))
          (↑(X.presheaf.1 (Opposite.op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')))))
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')).hom'