-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma app_basicOpen_eq_away_map {X Y : Scheme.{u}} (f : X ⟶ Y) {U : Y.Opens}
    (hU : IsAffineOpen U) (h : IsAffineOpen (f ⁻¹ᵁ U)) (r : Γ(Y, U)) :
    haveI := hU.isLocalization_basicOpen r
    haveI := h.isLocalization_basicOpen (f.app U r)
    f.app (Y.basicOpen r) =
      (CommRingCat.ofHom
        (IsLocalization.Away.map Γ(Y, Y.basicOpen r) Γ(X, X.basicOpen (f.app U r)) (f.app U).hom r)
        ≫ X.presheaf.map (eqToHom (by simp)).op)

Proof state:
case hf.h
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ Scheme.Hom.app f (Y.basicOpen r)) =
    (CommRingCat.Hom.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op))).comp
      (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
simp

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (eqToHom ⋯).op

Tactic:
haveI := h.isLocalization_basicOpen (f.app U r)

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (eqToHom ⋯).op

Proof state:
case hf
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
          (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
            (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
            (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
        X.presheaf.map (eqToHom ⋯).op)

Tactic:
apply IsLocalization.ringHom_ext (.powers r)

Result:
case hf.h
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r))).comp (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom
              (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
                (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
                (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
            X.presheaf.map (eqToHom ⋯).op)).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r))

Proof state:
X✝ Y✝ : Scheme
U✝ : X✝.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X✝, U✝)
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ f ⁻¹ᵁ Y.basicOpen r = X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)

Tactic:
simp

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (eqToHom ⋯).op

Tactic:
ext : 1

Result:
case hf
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
          (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
            (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
            (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
        X.presheaf.map (eqToHom ⋯).op)

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (eqToHom ⋯).op

Tactic:
haveI := hU.isLocalization_basicOpen r

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (eqToHom ⋯).op

Proof state:
case hf.h
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r))).comp (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom
              (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
                (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
                (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
            X.presheaf.map (eqToHom ⋯).op)).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r))

Tactic:
rw [IsLocalization.Away.map, CommRingCat.hom_comp, RingHom.comp_assoc, CommRingCat.hom_ofHom,
  IsLocalization.map_comp, RingHom.algebraMap_toAlgebra,
  RingHom.algebraMap_toAlgebra, ← RingHom.comp_assoc, ← CommRingCat.hom_comp,
  ← CommRingCat.hom_comp, ← X.presheaf.map_comp]

Result:
case hf.h
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ Scheme.Hom.app f (Y.basicOpen r)) =
    (CommRingCat.Hom.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op))).comp
      (CommRingCat.Hom.hom (Scheme.Hom.app f U))