awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
e_1 :
  (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) =
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
            (structureSheaf (↑Γ(X, U) : Type u)))
          (op (PrimeSpectrum.basicOpen f))) :
      Type u)
e_2 :
  HEq.{u + 1} (α := CommSemiring (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)) CommRing.toCommSemiring (β :=
    CommSemiring
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
              (structureSheaf (↑Γ(X, U) : Type u)))
            (op (PrimeSpectrum.basicOpen f))) :
        Type u))
    CommRing.toCommSemiring
h :
  ∀ (r : (↑Γ(X, U) : Type u)),
    Eq (α := (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
      ((algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
          r :
        (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
      ((algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
          r :
        (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
⊢ RingHom.toAlgebra
      ((asIso (hU.basicOpenSectionsToAffine f)).commRingCatIsoToRingEquiv.toRingHom.comp
        (algebraMap (↑Γ(X, U) : Type u) (↑Γ(X, X.basicOpen f) : Type u))) =
    StructureSheaf.openAlgebra (↑Γ(X, U) : Type u) (op (PrimeSpectrum.basicOpen f))

Tactic:
apply Algebra.algebra_ext

Premises used: Algebra.algebra_ext
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
e_1 :
  (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) =
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
            (structureSheaf (↑Γ(X, U) : Type u)))
          (op (PrimeSpectrum.basicOpen f))) :
      Type u)
e_2 :
  HEq.{u + 1} (α := CommSemiring (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)) CommRing.toCommSemiring (β :=
    CommSemiring
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
              (structureSheaf (↑Γ(X, U) : Type u)))
            (op (PrimeSpectrum.basicOpen f))) :
        Type u))
    CommRing.toCommSemiring
r : (↑Γ(X, U) : Type u)
h :
  Eq.{u + 1} (α := (↑Γ(X, U) : Type u) →+* (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
    (algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
    (algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
⊢ Eq (α := (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
    ((algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
        r :
      (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
    ((algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
        r :
      (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
e_1 :
  (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) =
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
            (structureSheaf (↑Γ(X, U) : Type u)))
          (op (PrimeSpectrum.basicOpen f))) :
      Type u)
e_2 :
  HEq.{u + 1} (α := CommSemiring (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)) CommRing.toCommSemiring (β :=
    CommSemiring
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
              (structureSheaf (↑Γ(X, U) : Type u)))
            (op (PrimeSpectrum.basicOpen f))) :
        Type u))
    CommRing.toCommSemiring
r : (↑Γ(X, U) : Type u)
h :
  CommRingCat.Hom.hom
      (X.presheaf.map (homOfLE ⋯).op ≫
        Scheme.Hom.app hU.fromSpec (X.basicOpen f) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) =
    algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)
⊢ Eq.{u + 1} (α := (↑Γ(X, U) : Type u) →+* (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
    (algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
    (algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))

Tactic:
dsimp [CommRingCat.ofHom, RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
    basicOpenSectionsToAffine]

Premises used: CommRingCat.ofHom, CommRingCat.hom_comp, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
e_1 :
  (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) =
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
            (structureSheaf (↑Γ(X, U) : Type u)))
          (op (PrimeSpectrum.basicOpen f))) :
      Type u)
e_2 :
  HEq.{u + 1} (α := CommSemiring (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)) CommRing.toCommSemiring (β :=
    CommSemiring
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
              (structureSheaf (↑Γ(X, U) : Type u)))
            (op (PrimeSpectrum.basicOpen f))) :
        Type u))
    CommRing.toCommSemiring
r : (↑Γ(X, U) : Type u)
h :
  CommRingCat.Hom.hom
      ((Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫
        (Spec Γ(X, U)).presheaf.map ((Opens.map hU.fromSpec.base).map (homOfLE ⋯).op.unop).op ≫
          (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) =
    algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)
⊢ CommRingCat.Hom.hom
      (X.presheaf.map (homOfLE ⋯).op ≫
        Scheme.Hom.app hU.fromSpec (X.basicOpen f) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) =
    algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)

Tactic:
rw [hU.fromSpec.naturality_assoc, hU.fromSpec_app_self]

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpec, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.Scheme.Hom.naturality_assoc
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
e_1 :
  (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) =
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
            (structureSheaf (↑Γ(X, U) : Type u)))
          (op (PrimeSpectrum.basicOpen f))) :
      Type u)
e_2 :
  HEq.{u + 1} (α := CommSemiring (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)) CommRing.toCommSemiring (β :=
    CommSemiring
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
              (structureSheaf (↑Γ(X, U) : Type u)))
            (op (PrimeSpectrum.basicOpen f))) :
        Type u))
    CommRing.toCommSemiring
r : (↑Γ(X, U) : Type u)
⊢ CommRingCat.Hom.hom
      ((Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫
        (Spec Γ(X, U)).presheaf.map ((Opens.map hU.fromSpec.base).map (homOfLE ⋯).op.unop).op ≫
          (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) =
    algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
inst : IsAffine X
r : (↑Γ(X, ⊤) : Type u)
⊢ IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)

Tactic:
isLocalization_basicOpen (isAffineOpen_top X) r

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X_1 Y_1 : Scheme
U_1 : X_1.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X_1, U_1) : Type u)
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : (↑Γ(Y, U) : Type u)
this_1 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u) := ⋯
this : IsLocalization.Away (R := (↑Γ(X, V) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
      r :
    (↑Γ(X, V) : Type u))
  (↑Γ(X,
        X.basicOpen (U := V)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
              (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
            r)) :
    Type u) :=
  ⋯
⊢ X.basicOpen (U := V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
        r) ≤
    f ⁻¹ᵁ Y.basicOpen r

Tactic:
simp [Scheme.Hom.appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : (↑Γ(Y, U) : Type u)
this_1 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u) := ⋯
this : IsLocalization.Away (R := (↑Γ(X, V) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
      r :
    (↑Γ(X, V) : Type u))
  (↑Γ(X,
        X.basicOpen (U := V)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
              (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
            r)) :
    Type u) :=
  ⋯
hf :
  CommRingCat.Hom.hom
      (Scheme.Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := V)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
              (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
            r))
        ⋯) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))) : Type u)
          (↑(X.presheaf.1
                (op
                  (X.basicOpen (U := V)
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
                        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
                      r)))) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r))
⊢ Scheme.Hom.appLE f (Y.basicOpen r)
      (X.basicOpen (U := V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
            (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
          r))
      ⋯ =
    CommRingCat.ofHom
      (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))) : Type u)
        (↑(X.presheaf.1
              (op
                (X.basicOpen (U := V)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
                      (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
                    r)))) :
          Type u)
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r)

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X_1 Y_1 : Scheme
U_1 : X_1.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X_1, U_1) : Type u)
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
this_1 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (↑Γ(X,
          X.basicOpen (U := f ⁻¹ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.app f U) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
              r)) :
      Type u)
⊢ f ⁻¹ᵁ Y.basicOpen r =
    X.basicOpen (U := f ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
        r)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
⊢ IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)

Tactic:
haveI := hU.isLocalization_basicOpen r
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
this : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
⊢ IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (↑Γ(X,
          X.basicOpen (U := f ⁻¹ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.app f U) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
              r)) :
      Type u)

Tactic:
haveI := h.isLocalization_basicOpen (f.app U r)
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
this_1 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (↑Γ(X,
          X.basicOpen (U := f ⁻¹ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.app f U) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
              r)) :
      Type u)
hf :
  CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
          (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
            (↑Γ(X,
                  X.basicOpen (U := f ⁻¹ᵁ U)
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (Scheme.Hom.app f U) :
                        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                      r)) :
              Type u)
            (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
        X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ U)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.app f U) :
                      (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                    r)) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
this_1 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (↑Γ(X,
          X.basicOpen (U := f ⁻¹ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.app f U) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
              r)) :
      Type u)
hf :
  Eq (α := (↑Γ(Y, U) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
    (RingHom.comp (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)))
      (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))
    (RingHom.comp (β := (↑Γ(Y, Y.basicOpen r) : Type u))
      (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
              (↑Γ(X,
                    X.basicOpen (U := f ⁻¹ᵁ U)
                      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := CommRingCat.carrier) (Scheme.Hom.app f U) :
                          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                        r)) :
                Type u)
              (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
          X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))))
      (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))
⊢ CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
          (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
            (↑Γ(X,
                  X.basicOpen (U := f ⁻¹ᵁ U)
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (Scheme.Hom.app f U) :
                        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                      r)) :
              Type u)
            (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
        X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
apply IsLocalization.ringHom_ext (.powers r)

Premises used: Submonoid.powers, IsLocalization.ringHom_ext
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
this_1 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (↑Γ(X,
          X.basicOpen (U := f ⁻¹ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.app f U) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
              r)) :
      Type u)
hf :
  CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ Scheme.Hom.app f (Y.basicOpen r)) =
    (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯)))).comp
      (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ Eq (α := (↑Γ(Y, U) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
    (RingHom.comp (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)))
      (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))
    (RingHom.comp (β := (↑Γ(Y, Y.basicOpen r) : Type u))
      (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
              (↑Γ(X,
                    X.basicOpen (U := f ⁻¹ᵁ U)
                      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := CommRingCat.carrier) (Scheme.Hom.app f U) :
                          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                        r)) :
                Type u)
              (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
          X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))))
      (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))

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]

Premises used: IsLocalization.map_comp, CommRingCat.hom_comp, RingHom.comp_assoc, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, IsLocalization.Away.map, CommRingCat.hom_ofHom, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, RingHom.algebraMap_toAlgebra, AlgebraicGeometry.Scheme.toLocallyRingedSpace