awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski (goal)
Goal:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
⊢ (∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
        (F.map (homOfLE ⋯).op)) ↔
    ∀ (U : X.AffineZariskiSite) (f : (↑Γ(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))
            f :
          (↑(F.obj (Opposite.op U)) : Type u))
        (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
have refine : ∀ (U : X.AffineZariskiSite) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
  IsPushout (X.presheaf.map (homOfLE sorry).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
      (F.map (homOfLE sorry).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) (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))
          f :
        (↑(F.obj (Opposite.op U)) : Type u))
      (↑(F.obj (Opposite.op (U.basicOpen f))) : Type u)
Tactic: refine forall₂_congr fun U f ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski (hypothesis)
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) :=
  ⋯
⊢ 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)
have 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)
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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski (hypothesis)
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)
⊢ 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)
have this₁ : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
Tactic: have : IsLocalization.Away f Γ(X, X.basicOpen f) := U.2.isLocalization_basicOpen _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski (goal)
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)
have 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)
Tactic: refine (CommRingCat.isPushout_iff_isPushout ..).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski (goal)
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)
      (↑(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)
have 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)
Tactic: rw [Algebra.IsPushout.comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski (goal)
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)
have refine : 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: refine (Algebra.isLocalization_iff_isPushout (.powers f) Γ(X, X.basicOpen f)).symm.trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski (hypothesis)
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)
⊢ 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)
have this : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski (goal)
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 ⋯)) =
    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)
have apply : (↑(Hom.opensRange ((relativeGluingData H).functor.map (homOfLE sorry))) : 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: apply TopologicalSpace.Opens.coe_inj.mp ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski (goal)
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
⊢ IsIso (X := (colimit.cocone F).pt) (Y := (cocone X).pt) (IsColimit.desc (colimit.isColimit F) (cocone X))
have refine : ∀ (U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) sorry).toPreZeroHypercover.1),
  MorphismProperty.isomorphisms Scheme (X :=
    PreZeroHypercover.X (S := (colimit.cocone F).pt)
      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
        (Precoverage.ZeroHypercover.pullback₁ (IsColimit.desc (colimit.isColimit F) (cocone X))
          (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) sorry)))
      U)
    (Cover.pullbackHom (P := IsOpenImmersion)
        (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) sorry)
        (IsColimit.desc (colimit.isColimit F) (cocone X)) U :
      PreZeroHypercover.X (S := (colimit.cocone F).pt)
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
            (Precoverage.ZeroHypercover.pullback₁ (IsColimit.desc (colimit.isColimit F) (cocone X))
              (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) sorry)))
          U ⟶
        (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) sorry).X U)
Tactic: refine (IsZariskiLocalAtTarget.iff_of_openCover (P := .isomorphisms _)
      (X.openCoverOfIsOpenCover _ (iSup_affineOpens_eq_top X))).mpr fun U ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski (goal)
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
⊢ MorphismProperty.isomorphisms Scheme (X :=
    PreZeroHypercover.X (S := (colimit.cocone F).pt)
      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
        (Precoverage.ZeroHypercover.pullback₁ (IsColimit.desc (colimit.isColimit F) (cocone X))
          (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)))
      U)
    (Cover.pullbackHom (P := IsOpenImmersion)
        (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)
        (IsColimit.desc (colimit.isColimit F) (cocone X)) U :
      PreZeroHypercover.X (S := (colimit.cocone F).pt)
          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
            (Precoverage.ZeroHypercover.pullback₁ (IsColimit.desc (colimit.isColimit F) (cocone X))
              (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)))
          U ⟶
        (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).X U)
have change : IsIso (X := pullback (X := colimit F) (colimit.desc F (cocone X)) (↑U : X.Opens).ι)
  (pullback.snd (colimit.desc F (cocone X)) (↑U : X.Opens).ι)
Tactic: change IsIso (pullback.snd (colimit.desc F (cocone X)) U.1.ι)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski (goal)
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
⊢ Eq (α := Set ↥(colimit F))
    (Set.range (ι := ↥(pullback (X := colimit F) (colimit.desc F (cocone X)) (↑U : X.Opens).ι))
      ⇑(pullback.fst (colimit.desc F (cocone X)) (↑U : X.Opens).ι))
    (Set.range (ι := ↥(↑(↑U : X.Opens) : Scheme)) ⇑((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U))
have rw : (↑(colimit.desc F (cocone X) ⁻¹ᵁ (↑U : X.Opens)) : Set ↥(colimit F)) =
  (↑(Hom.opensRange (colimit.ι F U)) : Set ↥(colimit F))
Tactic: rw [Pullback.range_fst, Opens.range_ι, ← Hom.coe_opensRange, Hom.opensRange_comp_of_isIso,
        ← Scheme.Hom.coe_preimage]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski (goal)
Goal:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).toPreZeroHypercover.1
⊢ (↑(colimit.desc F (cocone X) ⁻¹ᵁ (↑U : X.Opens)) : Set ↥(colimit F)) =
    (↑(Hom.opensRange (colimit.ι F U)) : Set ↥(colimit F))
have h : (cocone X).pt.Opens = X.Opens →
  HEq.{u + 2} (α := Category.{u, u} (cocone X).pt.Opens)
      (Preorder.smallCategory (TopologicalSpace.Opens ↥(cocone X).pt)) (β := Category.{u, u} X.Opens)
      (Preorder.smallCategory (TopologicalSpace.Opens ↥X)) →
    (↑(cocone X).pt.toPresheafedSpace : TopCat) = (↑X.toPresheafedSpace : TopCat) →
      (cocone X).pt.toPresheafedSpace = X.toPresheafedSpace →
        (cocone X).pt.toLocallyRingedSpace = X.toLocallyRingedSpace →
          (cocone X).pt = X → Eq (α := (colimit F).Hom (cocone X).pt) (colimit.desc F (cocone X)) D.toBase
Tactic: convert! congr($(D.toBase_preimage_eq_opensRange_ι U).1)