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
U : Opens (↑(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)
x : (↑(PrimeSpectrum.Top R) : Type u)
hx : x ∈ U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxV :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg :
  ∀ (x : ↥V),
    ∃ (hs : g ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
              ((iVU : (a : ↥V) → ↥(unop (op U))) x))
          x)
        (LocalizedModule.mk f
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) g hs))
g' : R
hxg' :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    (↑(basicOpen g') : Set (PrimeSpectrum R))
hg'U : (↑(basicOpen g') : Set (PrimeSpectrum R)) ⊆ (↑V : Set (↑(PrimeSpectrum.Top R) : Type u))
⊢ Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen g' ⊓ basicOpen g) x

Tactic:
exact ⟨hxg', (hfg ⟨x, hxV⟩).1⟩
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(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)
x : (↑(PrimeSpectrum.Top R) : Type u)
hx : x ∈ U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxV :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg :
  ∀ (x : ↥V),
    ∃ (hs : g ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
              ((iVU : (a : ↥V) → ↥(unop (op U))) x))
          x)
        (LocalizedModule.mk f
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) g hs))
g' : R
hxg' :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    (↑(basicOpen g') : Set (PrimeSpectrum R))
hg'U : (↑(basicOpen g') : Set (PrimeSpectrum R)) ⊆ (↑V : Set (↑(PrimeSpectrum.Top R) : Type u))
⊢ basicOpen g' ⊓ basicOpen g ≤ U

Tactic:
inf_le_left.trans (hg'U.trans iVU.le)

Premises used: Quiver.Hom.le, HasSubset.Subset.trans, inf_le_left, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(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)
x : (↑(PrimeSpectrum.Top R) : Type u)
hx : x ∈ U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxV :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg :
  ∀ (x : ↥V),
    ∃ (hs : g ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
              ((iVU : (a : ↥V) → ↥(unop (op U))) x))
          x)
        (LocalizedModule.mk f
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) g hs))
g' : R
hxg' :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    (↑(basicOpen g') : Set (PrimeSpectrum R))
hg'U : (↑(basicOpen g') : Set (PrimeSpectrum R)) ⊆ (↑V : Set (↑(PrimeSpectrum.Top R) : Type u))
⊢ basicOpen g' ⊓ basicOpen g ≤ U

Tactic:
exact inf_le_left.trans (hg'U.trans iVU.le)

Premises used: Quiver.Hom.le, HasSubset.Subset.trans, inf_le_left, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(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)
x : (↑(PrimeSpectrum.Top R) : Type u)
hx : x ∈ U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxV :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg :
  ∀ (x : ↥V),
    ∃ (hs : g ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
              ((iVU : (a : ↥V) → ↥(unop (op U))) x))
          x)
        (LocalizedModule.mk f
          (Subtype.mk (p := fun (x_2 : R) ↦ x_2 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) g hs))
g' : R
hxg' :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    (↑(basicOpen g') : Set (PrimeSpectrum R))
hg'U : (↑(basicOpen g') : Set (PrimeSpectrum R)) ⊆ (↑V : Set (↑(PrimeSpectrum.Top R) : Type u))
x_1 : ↥(unop (op (basicOpen (g' * g))))
y : (↑(PrimeSpectrum.Top R) : Type u)
hy : Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen (g' * g)))) y
⊢ Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen g' ⊓ basicOpen g))) y

Tactic:
rw [PrimeSpectrum.basicOpen_mul] at hy

Premises used: PrimeSpectrum.basicOpen_mul
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(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)
x : (↑(PrimeSpectrum.Top R) : Type u)
hx : x ∈ U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxV :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg :
  ∀ (x : ↥V),
    ∃ (hs : g ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
              ((iVU : (a : ↥V) → ↥(unop (op U))) x))
          x)
        (LocalizedModule.mk f
          (Subtype.mk (p := fun (x_2 : R) ↦ x_2 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) g hs))
g' : R
hxg' :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    (↑(basicOpen g') : Set (PrimeSpectrum R))
hg'U : (↑(basicOpen g') : Set (PrimeSpectrum R)) ⊆ (↑V : Set (↑(PrimeSpectrum.Top R) : Type u))
x_1 : ↥(unop (op (basicOpen (g' * g))))
y : (↑(PrimeSpectrum.Top R) : Type u)
hy_1 : Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen (g' * g)))) y
hy : Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen g' ⊓ basicOpen g))) y
⊢ g ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) y ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal

Tactic:
obtain ⟨hgy, H⟩ := hfg ⟨y, hg'U hy.1⟩

Premises used: Subtype.mk, And.left
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(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)
x : (↑(PrimeSpectrum.Top R) : Type u)
hx : x ∈ U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxV :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg :
  ∀ (x : ↥V),
    ∃ (hs : g ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
              ((iVU : (a : ↥V) → ↥(unop (op U))) x))
          x)
        (LocalizedModule.mk f
          (Subtype.mk (p := fun (x_2 : R) ↦ x_2 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) g hs))
g' : R
hxg' :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    (↑(basicOpen g') : Set (PrimeSpectrum R))
hg'U : (↑(basicOpen g') : Set (PrimeSpectrum R)) ⊆ (↑V : Set (↑(PrimeSpectrum.Top R) : Type u))
x_1 : ↥(unop (op (basicOpen (g' * g))))
y : (↑(PrimeSpectrum.Top R) : Type u)
hy_1 : Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen (g' * g)))) y
hy : Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen g' ⊓ basicOpen g))) y
hgy :
  g ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) y ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal
⊢ Eq (α :=
    Localizations M
      (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) y ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)))
    ((fun (x : ↥V) ↦
        (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          ((iVU : (a : ↥V) → ↥(unop (op U))) x))
      (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) y ⋯))
    (LocalizedModule.mk f
      (Subtype.mk (p := fun (x : R) ↦
        x ∈
          (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) y ⋯) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        g hgy))

Tactic:
obtain ⟨hgy, H⟩ := hfg ⟨y, hg'U hy.1⟩

Premises used: Subtype.mk, And.left
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(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)
x : (↑(PrimeSpectrum.Top R) : Type u)
hx : x ∈ U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxV :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg :
  ∀ (x : ↥V),
    ∃ (hs : g ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
              ((iVU : (a : ↥V) → ↥(unop (op U))) x))
          x)
        (LocalizedModule.mk f
          (Subtype.mk (p := fun (x_2 : R) ↦ x_2 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) g hs))
g' : R
hxg' :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U)) x hx) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    (↑(basicOpen g') : Set (PrimeSpectrum R))
hg'U : (↑(basicOpen g') : Set (PrimeSpectrum R)) ⊆ (↑V : Set (↑(PrimeSpectrum.Top R) : Type u))
x_1 : ↥(unop (op (basicOpen (g' * g))))
y : (↑(PrimeSpectrum.Top R) : Type u)
hy_1 : Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen (g' * g)))) y
hy : Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen g' ⊓ basicOpen g))) y
hgy :
  g ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) y ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal
H :
  Eq (α :=
    Localizations M
      (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) y ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)))
    ((fun (x : ↥V) ↦
        (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          ((iVU : (a : ↥V) → ↥(unop (op U))) x))
      (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) y ⋯))
    (LocalizedModule.mk f
      (Subtype.mk (p := fun (x : R) ↦
        x ∈
          (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) y ⋯) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        g hgy))
⊢ (g * g') • f = (g' * g) • f

Tactic:
ring_nf
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M
g : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu : U ≤ basicOpen g
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hv : V ≤ basicOpen g
i : op U ⟶ op V
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op V)))
    ((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))
              i) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op V)))
        (const f g U hu) :
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op V)))
    (const f g V hv :
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op V))

Tactic:
rfl

Premises used: Set.Mem, setOf, Quotient.mk', AlgebraicGeometry.StructureSheaf.const, OreLocalization.oreDiv, rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu : U ≤ basicOpen f
x : ↥(unop (op U))
simp :
  Eq.{u + 1} (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) 0
    ((↑0 : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x)
⊢ Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
    ((↑(const 0 f U hu) : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x :
      Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
    ((↑0 : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x :
      Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))

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
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu : U ≤ basicOpen f
x : ↥(unop (op U))
⊢ Eq.{u + 1} (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) 0
    ((↑0 : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R A : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu : U ≤ basicOpen f
x : ↥(unop (op U))
⊢ HSMul.hSMul (α := ↥(↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) 1
      (HSMul.hSMul (α := ↥(↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) (β := A) 1
        ((algebraMap R A : (a : R) → A) f : A)) =
    HSMul.hSMul (α := ↥(↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) 1
      (HSMul.hSMul (α := ↥(↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) (β := A)
        (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) f ⋯) 1)

Tactic:
simp [Algebra.smul_def, Submonoid.smul_def]

Premises used: Submonoid.smul_def, Algebra.smul_def
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
f : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu : U ≤ basicOpen f
⊢ Eq (α :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R R))
      (op U))
    (const f f U hu) 1

Tactic:
const_algebraMap ..

Premises used: AlgebraicGeometry.StructureSheaf.const_algebraMap
-- 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
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
⊢ U ≤ basicOpen 1

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R A : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
⊢ Eq (α :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R A))
      (op U))
    (const 1 1 U ⋯) 1

Tactic:
simpa using const_algebraMap 1 (A := A) U

Premises used: AlgebraicGeometry.StructureSheaf.const_algebraMap, OfNat.ofNat
-- 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₁ f₂ : M
g₁ g₂ : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ U ≤ basicOpen (g₁ * g₂)

Tactic:
simp [*, PrimeSpectrum.basicOpen_mul]

Premises used: PrimeSpectrum.basicOpen_mul
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : M
g₁ g₂ : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ HAdd.hAdd (α :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op U))
      (const f₁ g₁ U hu₁) (const f₂ g₂ U hu₂) =
    const (g₂ • f₁ + g₁ • f₂) (g₁ * g₂) U ⋯

Tactic:
Subtype.ext <| funext fun _ ↦ LocalizedModule.mk_add_mk

Premises used: LocalizedModule.mk_add_mk, funext, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M
r g : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu : U ≤ basicOpen g
⊢ HSMul.hSMul (β :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op U))
      r (const f g U hu) =
    const (r • f) g U hu

Tactic:
Subtype.ext <| funext fun _ ↦ LocalizedModule.smul'_mk _ _ _

Premises used: AlgebraicGeometry.StructureSheaf.const._proof_2, LocalizedModule.smul'_mk, Subtype.mk, funext, 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₁ f₂ : A
g₁ g₂ : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ U ≤ basicOpen (g₁ * g₂)

Tactic:
simp [*, PrimeSpectrum.basicOpen_mul]

Premises used: PrimeSpectrum.basicOpen_mul
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R A : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f₁ f₂ : A
g₁ g₂ : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ HMul.hMul (α :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R A))
        (op U))
      (const f₁ g₁ U hu₁) (const f₂ g₂ U hu₂) =
    const (f₁ * f₂) (g₁ * g₂) U ⋯

Tactic:
Subtype.ext <| funext fun _ ↦ LocalizedModule.mk_mul_mk

Premises used: LocalizedModule.mk_mul_mk, funext, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : M
g₁ g₂ : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
h : g₂ • f₁ = g₁ • f₂
x : ↥(unop (op U))
⊢ ∃ (u : ↥(↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl),
    u •
        HSMul.hSMul (α := ↥(↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) g₂ ⋯)
          f₁ =
      u •
        HSMul.hSMul (α := ↥(↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) g₁ ⋯) f₂

Tactic:
simp [h, Submonoid.smul_def]

Premises used: Submonoid.smul_def
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : M
g₁ g₂ : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu : U ≤ basicOpen g₁
hf : f₁ = f₂
hg : g₁ = g₂
substs :
  Eq (α :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op U))
    (const f₁ g₁ U hu) (const f₁ g₁ U ⋯)
⊢ Eq (α :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op U))
    (const f₁ g₁ U hu) (const f₂ g₂ U ⋯)

Tactic:
substs hf hg
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ : M
g₁ : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu : U ≤ basicOpen g₁
⊢ Eq (α :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op U))
    (const f₁ g₁ U hu) (const f₁ g₁ U ⋯)

Tactic:
rfl