awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
set :
  let αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f));
  IsPushout (X.presheaf.map (homOfLE ⋯).op) αU αUf (F.map (homOfLE ⋯).op) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) αU :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
⊢ IsPushout (X.presheaf.map (homOfLE ⋯).op) αU (α.app (Opposite.op (U.basicOpen f))) (F.map (homOfLE ⋯).op) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) αU :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)

Tactic:
set αUf : Γ(X, X.basicOpen f) ⟶ F.obj (.op (U.basicOpen f)) := α.app (.op (U.basicOpen f))

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen, Opposite.op, AlgebraicGeometry.Scheme.basicOpen, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u) := (CommRingCat.Hom.hom αU).toAlgebra
algInst_1 : Algebra (↑Γ(X, X.basicOpen f) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom αUf).toAlgebra
algInst_2 : Algebra (↑(F.obj (Opposite.op U)) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst_3 : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u)
  (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ⋯
⊢ IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
    (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)

Tactic:
have : IsScalarTower Γ(X, U.toOpens) Γ(X, X.basicOpen f) (F.obj (.op (U.basicOpen f))) :=
    .of_algebraMap_eq' congr($(α.naturality (U.basicOpen_le f).hom.op).hom).symm
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u) := (CommRingCat.Hom.hom αU).toAlgebra
algInst_1 : Algebra (↑Γ(X, X.basicOpen f) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom αUf).toAlgebra
algInst_2 : Algebra (↑(F.obj (Opposite.op U)) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst_3 : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u)
  (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ⋯
this :
  IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
    (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)

Tactic:
have : IsLocalization.Away f Γ(X, X.basicOpen f) := U.2.isLocalization_basicOpen _
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u) := (CommRingCat.Hom.hom αU).toAlgebra
algInst_1 : Algebra (↑Γ(X, X.basicOpen f) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom αUf).toAlgebra
algInst_2 : Algebra (↑(F.obj (Opposite.op U)) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst_3 : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u)
  (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ⋯
this_1 :
  IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
    (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
⊢ IsPushout (X.presheaf.map (homOfLE ⋯).op) αU αUf (F.map (homOfLE ⋯).op) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) αU :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)

Tactic:
(CommRingCat.isPushout_iff_isPushout ..).trans ?_

Premises used: Set.Mem, setOf, AlgebraicGeometry.RingedSpace.basicOpen, CommRingCat.isPushout_iff_isPushout, AlgebraicGeometry.Scheme.basicOpen, Iff.trans
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u) := (CommRingCat.Hom.hom αU).toAlgebra
algInst_1 : Algebra (↑Γ(X, X.basicOpen f) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom αUf).toAlgebra
algInst_2 : Algebra (↑(F.obj (Opposite.op U)) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst_3 : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u)
  (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ⋯
this_1 :
  IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
    (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
refine :
  Algebra.IsPushout.{u, u, u, u} (↑(X.presheaf.1 (Opposite.op (↑U : X.Opens))) : Type u)
      (↑(X.presheaf.1 (Opposite.op (X.basicOpen f))) : Type u) (↑(F.1 (Opposite.op U)) : Type u)
      (↑(F.1 (Opposite.op (U.basicOpen f))) : Type u) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) αU :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
⊢ IsPushout (X.presheaf.map (homOfLE ⋯).op) αU αUf (F.map (homOfLE ⋯).op) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) αU :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)

Tactic:
refine (CommRingCat.isPushout_iff_isPushout ..).trans ?_

Premises used: CommRingCat.isPushout_iff_isPushout, Iff.trans
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u) := (CommRingCat.Hom.hom αU).toAlgebra
algInst_1 : Algebra (↑Γ(X, X.basicOpen f) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom αUf).toAlgebra
algInst_2 : Algebra (↑(F.obj (Opposite.op U)) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst_3 : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u)
  (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ⋯
this_1 :
  IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
    (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
rw :
  Algebra.IsPushout.{u, u, u, u} (↑(X.presheaf.1 (Opposite.op (↑U : X.Opens))) : Type u)
      (↑(F.1 (Opposite.op U)) : Type u) (↑(X.presheaf.1 (Opposite.op (X.basicOpen f))) : Type u)
      (↑(F.1 (Opposite.op (U.basicOpen f))) : Type u) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) αU :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
⊢ Algebra.IsPushout.{u, u, u, u} (↑(X.presheaf.1 (Opposite.op (↑U : X.Opens))) : Type u)
      (↑(X.presheaf.1 (Opposite.op (X.basicOpen f))) : Type u) (↑(F.1 (Opposite.op U)) : Type u)
      (↑(F.1 (Opposite.op (U.basicOpen f))) : Type u) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) αU :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)

Tactic:
rw [Algebra.IsPushout.comm]

Premises used: Algebra.IsPushout.comm
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u) := (CommRingCat.Hom.hom αU).toAlgebra
algInst_1 : Algebra (↑Γ(X, X.basicOpen f) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom αUf).toAlgebra
algInst_2 : Algebra (↑(F.obj (Opposite.op U)) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst_3 : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u)
  (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ⋯
this_1 :
  IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
    (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
⊢ Algebra.IsPushout.{u, u, u, u} (↑(X.presheaf.1 (Opposite.op (↑U : X.Opens))) : Type u)
      (↑(F.1 (Opposite.op U)) : Type u) (↑(X.presheaf.1 (Opposite.op (X.basicOpen f))) : Type u)
      (↑(F.1 (Opposite.op (U.basicOpen f))) : Type u) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) αU :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)

Tactic:
(Algebra.isLocalization_iff_isPushout (.powers f) Γ(X, X.basicOpen f)).symm.trans ?_

Premises used: CommRingCat.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, Submonoid.powers, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.presheaf, Iff.trans, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Iff.symm, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace, Algebra.isLocalization_iff_isPushout
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u) := (CommRingCat.Hom.hom αU).toAlgebra
algInst_1 : Algebra (↑Γ(X, X.basicOpen f) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom αUf).toAlgebra
algInst_2 : Algebra (↑(F.obj (Opposite.op U)) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst_3 : Algebra (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑(F.obj (Opposite.op U)) : Type u)
  (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u) :=
  ⋯
this_1 :
  IsScalarTower.{u, u, u} (↑Γ(X, U.toOpens) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
    (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
⊢ IsLocalization (R := (↑(F.1 (Opposite.op U)) : Type u))
      (Algebra.algebraMapSubmonoid (↑(F.1 (Opposite.op U)) : Type u) (Submonoid.powers f))
      (↑(F.1 (Opposite.op (U.basicOpen f))) : Type u) ↔
    IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) αU :
            (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
              (↑(F.obj (Opposite.op U)) : Type u))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H : NatTrans.Coequifibered α
⊢ ((F.rightOp ⋙ Scheme.Spec) ⋙ forget).IsLocallyDirected

Tactic:
(relativeGluingData H).instIsLocallyDirectedI₀CompFunctorForgetOfIsThin

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite, AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData, CategoryTheory.Functor.comp, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H : NatTrans.Coequifibered α
⊢ ∀ ⦃U V : X.AffineZariskiSite⦄ (f : U ⟶ V), IsOpenImmersion ((F.rightOp ⋙ Scheme.Spec).map f)

Tactic:
fun U V ↦ (relativeGluingData H).instIsOpenImmersionMapI₀Functor

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H : NatTrans.Coequifibered α
⊢ ∀ ⦃U V : X.AffineZariskiSite⦄ (f : U ⟶ V), IsOpenImmersion ((F.rightOp ⋙ Scheme.Spec).map f)

Tactic:
exact fun U V ↦ (relativeGluingData H).instIsOpenImmersionMapI₀Functor

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H : NatTrans.Coequifibered α
U : X.AffineZariskiSite
r : (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
            (α.app (Opposite.op U)) :
          (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
            (↑(F.obj (Opposite.op U)) : Type u))
        r :
      (↑(F.obj (Opposite.op U)) : Type u))
    (↑(F.obj (Opposite.op (U.basicOpen r))) : Type u)

Tactic:
have := coequifibered_iff_forall_isLocalizationAway.mp H U r
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H : NatTrans.Coequifibered α
U : X.AffineZariskiSite
r : (↑Γ(X, (↑U : X.Opens)) : Type u)
this_1 :
  IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
            (α.app (Opposite.op U)) :
          (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
            (↑(F.obj (Opposite.op U)) : Type u))
        r :
      (↑(F.obj (Opposite.op U)) : Type u))
    (↑(F.obj (Opposite.op (U.basicOpen r))) : Type u)
this : Algebra (↑(F.obj (Opposite.op U)) : Type u) (↑(F.obj (Opposite.op (U.basicOpen r))) : Type u) :=
  (CommRingCat.Hom.hom (F.map (homOfLE ⋯).op)).toAlgebra
apply :
  (↑(Hom.opensRange ((relativeGluingData H).functor.map (homOfLE ⋯))) : Set ↥((relativeGluingData H).functor.obj U)) =
    (↑(PrimeSpectrum.basicOpen
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
                  (α.app (Opposite.op U)) :
                (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
                  (↑(F.obj (Opposite.op U)) : Type u))
              r) :
          TopologicalSpace.Opens (PrimeSpectrum (↑(F.obj (Opposite.op U)) : Type u))) :
      Set ↥((relativeGluingData H).functor.obj U))
⊢ Hom.opensRange ((relativeGluingData H).functor.map (homOfLE ⋯)) =
    PrimeSpectrum.basicOpen
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
            (α.app (Opposite.op U)) :
          (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
            (↑(F.obj (Opposite.op U)) : Type u))
        r)

Tactic:
apply TopologicalSpace.Opens.coe_inj.mp ?_

Premises used: Iff.mp, TopologicalSpace.Opens.coe_inj
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
H : NatTrans.Coequifibered α
U : X.AffineZariskiSite
r : (↑Γ(X, (↑U : X.Opens)) : Type u)
this_1 :
  IsLocalization.Away (R := (↑(F.obj (Opposite.op U)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
            (α.app (Opposite.op U)) :
          (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
            (↑(F.obj (Opposite.op U)) : Type u))
        r :
      (↑(F.obj (Opposite.op U)) : Type u))
    (↑(F.obj (Opposite.op (U.basicOpen r))) : Type u)
this : Algebra (↑(F.obj (Opposite.op U)) : Type u) (↑(F.obj (Opposite.op (U.basicOpen r))) : Type u) :=
  (CommRingCat.Hom.hom (F.map (homOfLE ⋯).op)).toAlgebra
⊢ (↑(Hom.opensRange ((relativeGluingData H).functor.map (homOfLE ⋯))) : Set ↥((relativeGluingData H).functor.obj U)) =
    (↑(PrimeSpectrum.basicOpen
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := ((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U))
                  (α.app (Opposite.op U)) :
                (a : (↑(((toOpensFunctor X).op ⋙ X.presheaf).obj (Opposite.op U)) : Type u)) →
                  (↑(F.obj (Opposite.op U)) : Type u))
              r) :
          TopologicalSpace.Opens (PrimeSpectrum (↑(F.obj (Opposite.op U)) : Type u))) :
      Set ↥((relativeGluingData H).functor.obj U))

Tactic:
PrimeSpectrum.localization_away_comap_range (F.obj (.op <| U.basicOpen r))
    (α.app (.op U) r)

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite, CommRingCat.carrier, CategoryTheory.ConcreteCategory.hom, setOf, AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen, Opposite.op, Set.range, PrimeSpectrum.comap, DFunLike.coe, PrimeSpectrum.localization_away_comap_range, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app