awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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)
⊢ Membership.mem (γ := Ideal R) (Ideal.span (Set.range b)) (f ^ n * f)

Tactic:
replace hn := Ideal.mul_mem_right f _ hn
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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)
⊢ ∃ (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

Premises used: pow_succ, Finsupp.mem_span_range_iff_exists_finsupp, Ideal.span
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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)
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
⊢ ∃ (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
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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)
⊢ ∀ (i : ι), HSMul.hSMul (α := R) 0 (b i) = 0

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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)
⊢ ∑ i : ι, HSMul.hSMul (α := R) ((c : (a : ι) → R) i : R) (b i) = f ^ (n + 1)

Tactic:
rw [Finsupp.sum_fintype _ _ (by simp)] at hc

Premises used: Finsupp.sum_fintype
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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

Tactic:
⟨LocalizedModule.mk (∑ i, c i • a i) ⟨f ^ (n + 1), _, rfl⟩, ?_⟩

Premises used: Finset.univ, LocalizedModule.mk, Subtype.mk, HPow.hPow, HAdd.hAdd, Exists.intro, HSMul.hSMul, OfNat.ofNat, DFunLike.coe, Finset.sum, rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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)
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)) ⋯)) =
    s
⊢ ∃ (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:
refine ⟨LocalizedModule.mk (∑ i, c i • a i) ⟨f ^ (n + 1), _, rfl⟩, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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)
⊢ (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)) ⋯)) =
    s

Tactic:
(structureSheafInType R M).eq_of_locally_eq' (fun i ↦ basicOpen (b i)) _
    (fun i ↦ (ibU _).hom) iU _ _ fun i ↦ (Subtype.ext (funext fun x ↦ ?_)).trans (H _).symm

Premises used: PrimeSpectrum.basicOpen, LE.le.hom, funext, TopCat.Sheaf.eq_of_locally_eq', AlgebraicGeometry.structureSheafInType, Eq.symm, Eq.trans, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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 (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)))
    (Submonoid.powers 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)

Tactic:
IsLocalizedModule.of_linearEquiv (.powers f) (LocalizedModule.mkLinearMap (.powers f) M)
      (.ofBijective _ ⟨toBasicOpenₗ_injective _, toBasicOpenₗ_surjective _⟩)

Premises used: _private.0.AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_injective, And.intro, Submonoid.powers, LocalizedModule.mkLinearMap, IsLocalizedModule.of_linearEquiv, LinearEquiv.ofBijective, _private.0.AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_surjective
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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
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) ⋯) :
        LocalizedModule (Submonoid.powers f) M →ₗ[R] (structureSheafInType R M).obj.obj (op (basicOpen f))) ∘ₗ
      LocalizedModule.mkLinearMap (Submonoid.powers f) M)
⊢ 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))

Tactic:
convert!
    IsLocalizedModule.of_linearEquiv (.powers f) (LocalizedModule.mkLinearMap (.powers f) M)
      (.ofBijective _ ⟨toBasicOpenₗ_injective _, toBasicOpenₗ_surjective _⟩)

Premises used: _private.0.AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_injective, And.intro, Submonoid.powers, LocalizedModule.mkLinearMap, IsLocalizedModule.of_linearEquiv, LinearEquiv.ofBijective, _private.0.AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_surjective
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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
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) ⋯) :
                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)))
⊢ 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)

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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
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) ⋯) :
              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:
simp [toOpenₗ]

Premises used: AlgebraicGeometry.StructureSheaf.toOpenₗ