awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
h : g (↑j : ↥U) ^ (N + 1) • g (↑i : ↥U) ^ N • f (↑i : ↥U) = (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑j : ↥U) • f (↑i : ↥U)
h₁ : g (↑i : ↥U) ^ (N + 1) • g (↑j : ↥U) ^ N • f (↑j : ↥U) = (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑i : ↥U) • f (↑j : ↥U)
⊢ g (↑j : ↥U) ^ (N + 1) • g (↑i : ↥U) ^ N • f (↑i : ↥U) = g (↑i : ↥U) ^ (N + 1) • g (↑j : ↥U) ^ N • f (↑j : ↥U)
have refine_1 : (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑j : ↥U) • f (↑i : ↥U) =
  (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑i : ↥U) • f (↑j : ↥U)
Tactic: convert_to (g i * g ↑j) ^ N • g j • f i = (g i * g ↑j) ^ N • g i • f j
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (hypothesis)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
⊢ (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑j : ↥U) • f (↑i : ↥U) =
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑i : ↥U) • f (↑j : ↥U)
have this : n (↑i : ↥U) (↑j : ↥U) + 1 ≤ N
Tactic: have : n i j + 1 ≤ N := (t ×ˢ t).le_sup (f := fun x ↦ n x.1 x.2 + 1) (b := ⟨_, _⟩) (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
this : n (↑i : ↥U) (↑j : ↥U) + 1 ≤ N
⊢ (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑j : ↥U) • f (↑i : ↥U) =
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ N • g (↑i : ↥U) • f (↑j : ↥U)
have refine_1 : (g (↑i : ↥U) * g (↑j : ↥U)) ^ (N - (n (↑i : ↥U) (↑j : ↥U) + 1)) •
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
  (g (↑i : ↥U) * g (↑j : ↥U)) ^ (N - (n (↑i : ↥U) (↑j : ↥U) + 1)) •
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑i : ↥U) • f (↑j : ↥U)
Tactic: rw [← Nat.sub_add_cancel this, pow_add, mul_smul, mul_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
this : n (↑i : ↥U) (↑j : ↥U) + 1 ≤ N
⊢ (g (↑i : ↥U) * g (↑j : ↥U)) ^ (N - (n (↑i : ↥U) (↑j : ↥U) + 1)) •
      (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ (N - (n (↑i : ↥U) (↑j : ↥U) + 1)) •
      (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑i : ↥U) • f (↑j : ↥U)
have refine_1 : (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
  (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑i : ↥U) • f (↑j : ↥U)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
this : n (↑i : ↥U) (↑j : ↥U) + 1 ≤ N
⊢ (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑i : ↥U) • f (↑j : ↥U)
have h : (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
  ((g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) * g (↑j : ↥U)) • f (↑i : ↥U)
Tactic: convert! (hn i j).symm using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i j : ↥t
this : n (↑i : ↥U) (↑j : ↥U) + 1 ≤ N
h :
  (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
    ((g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) * g (↑j : ↥U)) • f (↑i : ↥U)
⊢ (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑j : ↥U) • f (↑i : ↥U) =
    (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑i : ↥U) • f (↑j : ↥U)
have h₁ : (g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) • g (↑i : ↥U) • f (↑j : ↥U) =
  ((g (↑i : ↥U) * g (↑j : ↥U)) ^ (n (↑i : ↥U) (↑j : ↥U) + 1) * g (↑i : ↥U)) • f (↑j : ↥U)
Tactic: convert! (hn i j).symm using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
s :
  Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op (basicOpen f))
⊢ ∃ (a : LocalizedModule.Away f M),
    (toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f))) a = s
have obtain : ∀ (ι : Type u) (w : Fintype ι) (a : ι → M) (b : ι → R)
  (ibU : ∀ (i : ι), LE.le (α := Opens (PrimeSpectrum R)) (basicOpen (b i)) (basicOpen f))
  (iU : LE.le (α := Opens (↑(PrimeSpectrum.Top R) : Type u)) (basicOpen f) (⨆ (i : ι), basicOpen (b i)))
  (hab : ∀ (i j : ι), b j • a i = b i • a j)
  (H :
    ∀ (i : ι),
      Eq (α :=
        (fun (X : Type u) ↦ X)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (Sheaf.presheaf (structureSheafInType R M))
            (op (basicOpen (b i)))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryTheory.Functor.map (Sheaf.presheaf (structureSheafInType R M)) sorry.hom.op) :
              (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).presheaf.obj (op (basicOpen f)))) →
                (fun (X : Type u) ↦ X) ((structureSheafInType R M).presheaf.obj (op (basicOpen (b i)))))
            s :
          (fun (X : Type u) ↦ X)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (Sheaf.presheaf (structureSheafInType R M))
              (op (basicOpen (b i)))))
        (const (a i) (b i) (basicOpen (b i)) sorry :
          Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R M))
            (op (basicOpen (b i))))),
  ∃ (a : LocalizedModule.Away f M),
    (toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f))) a = s
Tactic: obtain ⟨ι, _, a, b, ibU, iU, hab, H⟩ := exists_le_iSup_basicOpen_and_smul_eq_smul_and_eq_const _
    (PrimeSpectrum.isCompact_basicOpen _) s
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (hypothesis)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
s :
  Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op (basicOpen f))
ι : Type u
w : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), LE.le (α := Opens (PrimeSpectrum R)) (basicOpen (b i)) (basicOpen f)
iU : LE.le (α := Opens (↑(PrimeSpectrum.Top R) : Type u)) (basicOpen f) (⨆ (i : ι), basicOpen (b i))
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (Sheaf.presheaf (structureSheafInType R M))
          (op (basicOpen (b i)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Sheaf.presheaf (structureSheafInType R M)) ⋯.hom.op) :
            (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).presheaf.obj (op (basicOpen f)))) →
              (fun (X : Type u) ↦ X) ((structureSheafInType R M).presheaf.obj (op (basicOpen (b i)))))
          s :
        (fun (X : Type u) ↦ X)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (Sheaf.presheaf (structureSheafInType R M))
            (op (basicOpen (b i)))))
      (const (a i) (b i) (basicOpen (b i)) ⋯ :
        Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op (basicOpen (b i))))
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span (Set.range b))) f
have this : Subset (α := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus (Set.range b)) (PrimeSpectrum.zeroLocus {f})
Tactic: have : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f} := by
      simpa [← SetLike.coe_subset_coe, ← Set.compl_iInter,
        ← PrimeSpectrum.zeroLocus_iUnion, PrimeSpectrum.Top] using iU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
s :
  Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op (basicOpen f))
ι : Type u
w : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), LE.le (α := Opens (PrimeSpectrum R)) (basicOpen (b i)) (basicOpen f)
iU : LE.le (α := Opens (↑(PrimeSpectrum.Top R) : Type u)) (basicOpen f) (⨆ (i : ι), basicOpen (b i))
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (Sheaf.presheaf (structureSheafInType R M))
          (op (basicOpen (b i)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Sheaf.presheaf (structureSheafInType R M)) ⋯.hom.op) :
            (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).presheaf.obj (op (basicOpen f)))) →
              (fun (X : Type u) ↦ X) ((structureSheafInType R M).presheaf.obj (op (basicOpen (b i)))))
          s :
        (fun (X : Type u) ↦ X)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (Sheaf.presheaf (structureSheafInType R M))
            (op (basicOpen (b i)))))
      (const (a i) (b i) (basicOpen (b i)) ⋯ :
        Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op (basicOpen (b i))))
this : Subset (α := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus (Set.range b)) (PrimeSpectrum.zeroLocus {f})
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span (Set.range b))) f
have rw : ∀ (x : PrimeSpectrum R),
  Membership.mem (γ := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus (Set.range b)) x → f ∈ x.asIdeal
Tactic: rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.zeroLocus_span,
      PrimeSpectrum.mem_vanishingIdeal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
s :
  Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op (basicOpen f))
ι : Type u
w : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), LE.le (α := Opens (PrimeSpectrum R)) (basicOpen (b i)) (basicOpen f)
iU : LE.le (α := Opens (↑(PrimeSpectrum.Top R) : Type u)) (basicOpen f) (⨆ (i : ι), basicOpen (b i))
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (Sheaf.presheaf (structureSheafInType R M))
          (op (basicOpen (b i)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Sheaf.presheaf (structureSheafInType R M)) ⋯.hom.op) :
            (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).presheaf.obj (op (basicOpen f)))) →
              (fun (X : Type u) ↦ X) ((structureSheafInType R M).presheaf.obj (op (basicOpen (b i)))))
          s :
        (fun (X : Type u) ↦ X)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (Sheaf.presheaf (structureSheafInType R M))
            (op (basicOpen (b i)))))
      (const (a i) (b i) (basicOpen (b i)) ⋯ :
        Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op (basicOpen (b i))))
⊢ ∃ (a : LocalizedModule.Away f M),
    (toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f))) a = s
have obtain : ∀ (n : ℕ) (hn : Membership.mem (γ := Ideal R) (Ideal.span (Set.range b)) (f ^ n)),
  ∃ (a : LocalizedModule.Away f M),
    (toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f))) a = s
Tactic: obtain ⟨n, hn⟩ : f ∈ (Ideal.span (Set.range b)).radical := by
    have : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f} := by
      simpa [← SetLike.coe_subset_coe, ← Set.compl_iInter,
        ← PrimeSpectrum.zeroLocus_iUnion, PrimeSpectrum.Top] using iU
    rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.zeroLocus_span,
      PrimeSpectrum.mem_vanishingIdeal]
    exact fun x hx ↦ by simpa using this hx