awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))))
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
have hn₁ : Membership.mem (γ := Ideal R) (Ideal.span (Set.range b)) (f ^ n * f)
Tactic: replace hn := Ideal.mul_mem_right f _ hn
Cleared hypotheses: hn
-- 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))))
n : ℕ
hn : Membership.mem (γ := Ideal R) (Ideal.span (Set.range b)) (f ^ n * 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 hn₁ : ∃ (c : ι →₀ R), (c.sum fun (i : ι) (a : R) ↦ a • b i) = f ^ (n + 1)
Tactic: rw [← pow_succ, Ideal.span, Finsupp.mem_span_range_iff_exists_finsupp] at hn
Cleared hypotheses: hn
-- 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))))
n : ℕ
hn : ∃ (c : ι →₀ R), (c.sum fun (i : ι) (a : R) ↦ a • b i) = f ^ (n + 1)
⊢ ∃ (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 : ∀ (c : ι →₀ R) (hc : (c.sum fun (i : ι) (a : R) ↦ a • b i) = f ^ (n + 1)),
  ∃ (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 ⟨c, hc⟩ := hn
Cleared hypotheses: hn
-- 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))))
n : ℕ
c : ι →₀ R
hc : (c.sum fun (i : ι) (a : R) ↦ a • b i) = f ^ (n + 1)
⊢ ∃ (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 hc₁ : ∑ i : ι, HSMul.hSMul (α := R) ((c : (a : ι) → R) i : R) (b i) = f ^ (n + 1)
Tactic: rw [Finsupp.sum_fintype _ _ (by simp)] at hc
Cleared hypotheses: hc
-- 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))))
n : ℕ
c : ι →₀ R
hc : ∑ i : ι, HSMul.hSMul (α := R) ((c : (a : ι) → R) i : R) (b i) = f ^ (n + 1)
⊢ ∃ (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 refine : (toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
    (LocalizedModule.mk (∑ i : ι, HSMul.hSMul (α := R) ((c : (a : ι) → R) i : R) (a i))
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers f) x) (f ^ (n + 1)) sorry)) =
  s
Tactic: refine ⟨LocalizedModule.mk (∑ i, c i • a i) ⟨f ^ (n + 1), _, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
f : R
⊢ IsLocalizedModule.Away (M' :=
    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)))
    f (toOpenₗ R M (basicOpen f))
have h : Eq (α :=
  M →ₗ[R]
    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)))
  (toOpenₗ R M (basicOpen f))
  ((↑(LinearEquiv.ofBijective (toBasicOpenₗ R M f) sorry) :
      LocalizedModule (Submonoid.powers f) M →ₗ[R] (structureSheafInType R M).obj.obj (op (basicOpen f))) ∘ₗ
    LocalizedModule.mkLinearMap (Submonoid.powers f) M)
Tactic: convert!
    IsLocalizedModule.of_linearEquiv (.powers f) (LocalizedModule.mkLinearMap (.powers f) M)
      (.ofBijective _ ⟨toBasicOpenₗ_injective _, toBasicOpenₗ_surjective _⟩)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
f : R
⊢ Eq (α :=
    M →ₗ[R]
      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)))
    (toOpenₗ R M (basicOpen f))
    ((↑(LinearEquiv.ofBijective (toBasicOpenₗ R M f) ⋯) :
        LocalizedModule (Submonoid.powers f) M →ₗ[R] (structureSheafInType R M).obj.obj (op (basicOpen f))) ∘ₗ
      LocalizedModule.mkLinearMap (Submonoid.powers f) M)
have h : ∀ (x : M),
  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 f)))
    ((toOpenₗ R M (basicOpen f) : (a : M) → (structureSheafInType R M).obj.obj (op (basicOpen f))) x :
      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)))
    (((↑(LinearEquiv.ofBijective (toBasicOpenₗ R M f) sorry) :
              LocalizedModule (Submonoid.powers f) M →ₗ[R] (structureSheafInType R M).obj.obj (op (basicOpen f))) ∘ₗ
            LocalizedModule.mkLinearMap (Submonoid.powers f) M :
          (a : M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        x :
      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)))
Tactic: ext x
-- 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
⊢ IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤)
have a : IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤) ↔
  IsLocalizedModule (M' :=
    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 1)))
    (Submonoid.powers 1) (toOpenₗ R M (basicOpen 1))
Tactic: convert! (inferInstance : IsLocalizedModule (.powers 1) (toOpenₗ R M (basicOpen 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
⊢ IsLocalizedModule (M' :=
      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 ⊤))
      ⊥ (toOpenₗ R M ⊤) ↔
    IsLocalizedModule (M' :=
      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 1)))
      (Submonoid.powers 1) (toOpenₗ R M (basicOpen 1))
have a : IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤) ↔
  IsLocalizedModule (M' :=
    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 ⊤))
    (Submonoid.powers 1) (toOpenₗ R M ⊤)
Tactic: rw [PrimeSpectrum.basicOpen_one, Submonoid.powers_one]
-- 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
a :
  IsLocalizedModule (M' :=
      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 ⊤))
      ⊥ (toOpenₗ R M ⊤) ↔
    IsLocalizedModule (M' :=
      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 ⊤))
      (Submonoid.powers 1) (toOpenₗ R M ⊤)
⊢ IsLocalizedModule (M' :=
      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 ⊤))
      ⊥ (toOpenₗ R M ⊤) ↔
    IsLocalizedModule (M' :=
      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 1)))
      (Submonoid.powers 1) (toOpenₗ R M (basicOpen 1))
have a₁ : IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤) ↔
  IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤)
Tactic: rw [PrimeSpectrum.basicOpen_one, Submonoid.powers_one]
-- 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
⊢ Function.Bijective (α := M) (β :=
    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 ⊤))
    (⇑(toOpenₗ R M ⊤) : (a : M) → (structureSheafInType R M).obj.obj (op ⊤))
have this : IsLocalizedModule (M' :=
  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 ⊤))
  ⊥ (toOpenₗ R M ⊤)
Tactic: have : IsLocalizedModule ⊥ (toOpenₗ R M ⊤) := by
    convert! (inferInstance : IsLocalizedModule (.powers 1) (toOpenₗ R M (basicOpen 1)))
    rw [PrimeSpectrum.basicOpen_one, Submonoid.powers_one]
-- 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
this :
  IsLocalizedModule (M' :=
    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 ⊤))
    ⊥ (toOpenₗ R M ⊤)
⊢ Function.Bijective (α := M) (β :=
    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 ⊤))
    (⇑(toOpenₗ R M ⊤) : (a : M) → (structureSheafInType R M).obj.obj (op ⊤))
have refine : ∀
  (x :
    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 ⊤)),
  ∃ (a : M), (toOpenₗ R M ⊤ : (a : M) → (structureSheafInType R M).obj.obj (op ⊤)) a = x
Tactic: refine ⟨fun x y e ↦ by simpa using (IsLocalizedModule.eq_iff_exists ⊥ _).mp e, fun x ↦ ?_⟩