awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → (↑R : Type u_2)
hs : Eq (α := Ideal (↑R : Type u_2)) (Ideal.span (Set.range s)) ⊤
x : ↥(Spec R)
⊢ Membership.mem (γ := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(Spec
          (CommRingCat.of
            (Localization.Away
              (s
                (have this : ∃ (i : ι), s i ∉ x.asIdeal := ⋯;
                this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal)))))))
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R : Type u_2)
              (Localization.Away
                (s
                  (have this : ∃ (i : ι), s i ∉ x.asIdeal := ⋯;
                  this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal))))))))
    x
have generalize_proofs : ∀ (H : ∃ (i : ι), s i ∉ x.asIdeal),
  Membership.mem (γ := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(Spec
          (CommRingCat.of
            (Localization.Away
              (s
                (have this := H;
                this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal)))))))
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R : Type u_2)
              (Localization.Away
                (s
                  (have this := H;
                  this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal))))))))
    x
Tactic: generalize_proofs H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (hypothesis)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → (↑R : Type u_2)
hs : Eq (α := Ideal (↑R : Type u_2)) (Ideal.span (Set.range s)) ⊤
x : ↥(Spec R)
H : ∃ (i : ι), s i ∉ x.asIdeal
i : ι := H.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal)
⊢ Membership.mem (γ := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(Spec
          (CommRingCat.of
            (Localization.Away
              (s
                (have this := H;
                this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal)))))))
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R : Type u_2)
              (Localization.Away
                (s
                  (have this := H;
                  this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal))))))))
    x
have this : Set.range (ι := PrimeSpectrum (Localization.Away (s i)))
    (PrimeSpectrum.comap (algebraMap (↑R : Type u_2) (Localization.Away (s i)))) =
  (↑(PrimeSpectrum.basicOpen (s i)) : Set (PrimeSpectrum (↑R : Type u_2)))
Tactic: have := PrimeSpectrum.localization_away_comap_range (Localization.Away (s i)) (s i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          f :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          g :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
⊢ f = g
have hcover : U ≤ ⨆ (i : ↥X), Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U
Tactic: fapply TopCat.Sheaf.eq_of_locally_eq' X.sheaf
    (fun i ↦ (𝒰.f (𝒰.idx i)).opensRange ⊓ U) _ (fun _ ↦ homOfLE inf_le_right)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          f :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          g :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
hcover : U ≤ ⨆ (i : ↥X), Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U
⊢ f = g
have h₁ : ∀ (i : ↥X),
  Eq (α :=
    (↑(X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
          (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj (op U))
            (Y :=
            X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
              (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U)))
            (X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).map (Quiver.Hom.op (homOfLE sorry))) :
          (a : (↑(X.sheaf.obj.obj (op U)) : Type u)) →
            (↑(X.sheaf.obj.obj (op (Hom.opensRange (𝒰.f (Cover.idx 𝒰 i)) ⊓ U))) : Type u))
        f :
      (↑(X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
            (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj (op U))
            (Y :=
            X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
              (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U)))
            (X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).map (Quiver.Hom.op (homOfLE sorry))) :
          (a : (↑(X.sheaf.obj.obj (op U)) : Type u)) →
            (↑(X.sheaf.obj.obj (op (Hom.opensRange (𝒰.f (Cover.idx 𝒰 i)) ⊓ U))) : Type u))
        g :
      (↑(X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
            (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U))) :
        Type u))
Tactic: fapply TopCat.Sheaf.eq_of_locally_eq' X.sheaf
    (fun i ↦ (𝒰.f (𝒰.idx i)).opensRange ⊓ U) _ (fun _ ↦ homOfLE inf_le_right)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          f :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          g :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
x : ↥X
hx : x ∈ U
⊢ Membership.mem (γ := TopologicalSpace.Opens ↥X)
    (⨆ (i : ↥X), Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U) x
have hcover : (∃ (x_1 : ↥X) (y : ↥(𝒰.X (Cover.idx 𝒰 x_1))), (𝒰.f (Cover.idx 𝒰 x_1)) y = x) ∧ x ∈ U
Tactic: simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_inf, Hom.coe_opensRange, Opens.mem_mk,
      Set.mem_iUnion, Set.mem_inter_iff, Set.mem_range, SetLike.mem_coe, exists_and_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          f :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          g :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
x : ↥X
hx : x ∈ U
⊢ (∃ (x_1 : ↥X) (y : ↥(𝒰.X (Cover.idx 𝒰 x_1))), (𝒰.f (Cover.idx 𝒰 x_1)) y = x) ∧ x ∈ U
have hcover : ∃ (x_1 : ↥X) (y : ↥(𝒰.X (Cover.idx 𝒰 x_1))), (𝒰.f (Cover.idx 𝒰 x_1)) y = x
Tactic: refine ⟨?_, hx⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
i : 𝒰.I₀
⊢ Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        0 :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
have rw : Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      s :
    (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
  (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
h :
  ∀ (i : 𝒰.I₀),
    IsNilpotent (R := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
⊢ IsNilpotent s
have choose : ∀ (fn : (i : 𝒰.I₀) → ℕ)
  (hfn :
    ∀ (i : 𝒰.I₀),
      HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
              s :
            (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          (fn i) =
        0),
  IsNilpotent s
Tactic: choose fn hfn using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
⊢ IsNilpotent s
have have : ∀ (this : Fintype 𝒰.I₀), IsNilpotent s
Tactic: have : Fintype 𝒰.I₀ := Fintype.ofFinite 𝒰.I₀
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (hypothesis)
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
this : Fintype 𝒰.I₀
N : ℕ := Finset.sup Finset.univ fn
⊢ IsNilpotent s
have hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
Tactic: have hfnleN (i : 𝒰.I₀) : fn i ≤ N := Finset.le_sup (Finset.mem_univ i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
this : Fintype 𝒰.I₀
N : ℕ := Finset.sup Finset.univ fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
⊢ IsNilpotent s
have h : s ^ N = 0
Tactic: use N
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
this : Fintype 𝒰.I₀
N : ℕ := Finset.sup Finset.univ fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
⊢ s ^ N = 0
have h : ∀ (i : 𝒰.I₀),
  Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (s ^ N) :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
Tactic: apply zero_of_zero_cover (𝒰 := 𝒰)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
this : Fintype 𝒰.I₀
N : ℕ := Finset.sup Finset.univ fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
i : 𝒰.I₀
⊢ Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (s ^ N) :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
have h : HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
    N =
  0
Tactic: simp only [map_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
U : X.Opens
s : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
fn : (i : 𝒰.I₀) → ℕ
hfn :
  ∀ (i : 𝒰.I₀),
    HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
        (fn i) =
      0
this : Fintype 𝒰.I₀
N : ℕ := Finset.sup Finset.univ fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
⊢ ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          (s ^ N) :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
have h : ∀ (i : 𝒰.I₀),
  HPow.hPow (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      N =
    0
Tactic: on_goal 1 => intro i; simp only [map_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
⊢ Membership.mem (γ := Set (Presieve (Spec R))) ((precoverage IsOpenImmersion).coverings (Spec R))
    (PreZeroHypercover.presieve₀
      { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
        f := fun (r : (↑R : Type u)) ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) })
have rw : (∀ (x : ↥(Spec R)),
    ∃ (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := Spec R)
        { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
          f := fun (r : (↑R : Type u)) ↦
            Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }),
      Membership.mem (γ := Set ↥(Spec R))
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
                f := fun (r : (↑R : Type u)) ↦
                  Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
                PreZeroHypercover (Spec R) }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
                f := fun (r : (↑R : Type u)) ↦
                  Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
                PreZeroHypercover (Spec R) }
              i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := Spec R)
        { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
          f := fun (r : (↑R : Type u)) ↦
            Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }),
    IsOpenImmersion
      (PreZeroHypercover.f
        { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
          f := fun (r : (↑R : Type u)) ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
          PreZeroHypercover (Spec R) }
        i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
⊢ (∀ (x : ↥(Spec R)),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := Spec R)
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }),
        Membership.mem (γ := Set ↥(Spec R))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
                  f := fun (r : (↑R : Type u)) ↦
                    Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
                  PreZeroHypercover (Spec R) }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
                  f := fun (r : (↑R : Type u)) ↦
                    Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
                  PreZeroHypercover (Spec R) }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := Spec R)
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
            PreZeroHypercover (Spec R) }
          i)
have refine : ∀ (x : ↥(Spec R)),
  Membership.mem (γ := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(PreZeroHypercover.X (S := Spec R)
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
            PreZeroHypercover (Spec R) }
          1))
      ⇑(PreZeroHypercover.f
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }
          1))
    x
Tactic: refine ⟨fun x ↦ ⟨1, ?_⟩, AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
⊢ Membership.mem (γ := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(PreZeroHypercover.X (S := Spec R)
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
            PreZeroHypercover (Spec R) }
          1))
      ⇑(PreZeroHypercover.f
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }
          1))
    x
have rw : Membership.mem (γ := Set ↥(Spec R)) Set.univ x
Tactic: rw [Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp _)]