awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
P : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha_1 :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule M U)))) a
x : ↥U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxV : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V
hVU : V ⟶ U
rx rs : R
hr :
  ∀ (x : ↥V),
    ∃ (hs : rs ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (↑r : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u))) ((hVU : (a : ↥V) → ↥U) x))
          x)
        (LocalizedModule.mk rx
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) rs hs))
W : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxW : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ W
hWU : W ⟶ U
ax : M
as : R
ha :
  ∀ (x : ↥W),
    ∃ (hs : as ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥W) ↦
            (a ((hWU : (a : ↥W) → ↥U) x) :
              Localizations (R := R) M (↑((hWU : (a : ↥W) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk ax
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) as hs))
refine :
  ∀ (y : ↥(V ⊓ W)),
    ∃ (hs : as * rs ∉ (↑y : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑y : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥(V ⊓ W)) ↦ (r • a) ((homOfLE ⋯ : (a : ↥(V ⊓ W)) → ↥U) x)) y)
        (LocalizedModule.mk (rx • ax)
          (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑y : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) (as * rs)
            hs))
⊢ ∃ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (_ : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U),
    PrelocalPredicate.pred (T := Localizations M) (isFractionPrelocal R M) (U := V) fun (x : ↥V) ↦
      (r • a) ((i : (a : ↥V) → ↥U) x)

Tactic:
refine ⟨V ⊓ W, ⟨hxV, hxW⟩, homOfLE (inf_le_left.trans hVU.le), rx • ax, as * rs, fun y ↦ ?_⟩
-- 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
P : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha_1 :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule M U)))) a
x : ↥U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxV : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V
hVU : V ⟶ U
rx rs : R
hr :
  ∀ (x : ↥V),
    ∃ (hs : rs ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (↑r : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u))) ((hVU : (a : ↥V) → ↥U) x))
          x)
        (LocalizedModule.mk rx
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) rs hs))
W : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxW : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ W
hWU : W ⟶ U
ax : M
as : R
ha :
  ∀ (x : ↥W),
    ∃ (hs : as ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥W) ↦
            (a ((hWU : (a : ↥W) → ↥U) x) :
              Localizations (R := R) M (↑((hWU : (a : ↥W) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk ax
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) as hs))
y : ↥(V ⊓ W)
⊢ rs ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) (↑y : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal

Tactic:
obtain ⟨hrsy, hry⟩ := hr ⟨y.1, y.2.1⟩

Premises used: Subtype.mk, And.left, Subtype.val, Subtype.property
-- 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
P : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha_1 :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule M U)))) a
x : ↥U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxV : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V
hVU : V ⟶ U
rx rs : R
hr :
  ∀ (x : ↥V),
    ∃ (hs : rs ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (↑r : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u))) ((hVU : (a : ↥V) → ↥U) x))
          x)
        (LocalizedModule.mk rx
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) rs hs))
W : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxW : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ W
hWU : W ⟶ U
ax : M
as : R
ha :
  ∀ (x : ↥W),
    ∃ (hs : as ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥W) ↦
            (a ((hWU : (a : ↥W) → ↥U) x) :
              Localizations (R := R) M (↑((hWU : (a : ↥W) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk ax
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) as hs))
y : ↥(V ⊓ W)
hrsy :
  rs ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) (↑y : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal
⊢ Eq (α :=
    Localizations R
      (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) (↑y : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)))
    ((fun (x : ↥V) ↦
        (↑r : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u))) ((hVU : (a : ↥V) → ↥U) x))
      (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) (↑y : (↑(PrimeSpectrum.Top R) : Type u))
        ⋯))
    (LocalizedModule.mk rx
      (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)) ⋯) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        rs hrsy))

Tactic:
obtain ⟨hrsy, hry⟩ := hr ⟨y.1, y.2.1⟩

Premises used: Subtype.mk, And.left, Subtype.val, Subtype.property
-- 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
P : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha_1 :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule M U)))) a
x : ↥U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxV : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V
hVU : V ⟶ U
rx rs : R
hr :
  ∀ (x : ↥V),
    ∃ (hs : rs ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (↑r : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u))) ((hVU : (a : ↥V) → ↥U) x))
          x)
        (LocalizedModule.mk rx
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) rs hs))
W : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxW : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ W
hWU : W ⟶ U
ax : M
as : R
ha :
  ∀ (x : ↥W),
    ∃ (hs : as ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥W) ↦
            (a ((hWU : (a : ↥W) → ↥U) x) :
              Localizations (R := R) M (↑((hWU : (a : ↥W) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk ax
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) as hs))
y : ↥(V ⊓ W)
hrsy :
  rs ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) (↑y : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal
hry :
  Eq (α :=
    Localizations R
      (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) (↑y : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)))
    ((fun (x : ↥V) ↦
        (↑r : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u))) ((hVU : (a : ↥V) → ↥U) x))
      (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ V) (↑y : (↑(PrimeSpectrum.Top R) : Type u))
        ⋯))
    (LocalizedModule.mk rx
      (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)) ⋯) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        rs hrsy))
⊢ as ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (↑y : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal

Tactic:
obtain ⟨hasy, hay⟩ := ha ⟨y.1, y.2.2⟩

Premises used: Subtype.mk, And.right, Subtype.val, Subtype.property
-- 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 t :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
x : ↥U
⊢ (↑(s + t) : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x =
    (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x +
      (↑t : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x

Tactic:
rfl

Premises used: rfl
-- 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)
s t :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R A))
    (op U)
x : ↥U
⊢ (↑(s * t) : (x : ↥(unop (op U))) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x =
    (↑s : (x : ↥(unop (op U))) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x *
      (↑t : (x : ↥(unop (op U))) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x

Tactic:
rfl

Premises used: rfl
-- 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)
r : R
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
x : ↥U
⊢ (↑(r • s) : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x =
    r • (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x

Tactic:
rfl

Premises used: rfl
-- 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))ᵒᵖ
⊢ IsScalarTower R
    (Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R R))
      U)
    (Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      U)

Tactic:
.of_algebraMap_smul fun r m ↦ Subtype.ext <| funext fun x ↦
    IsScalarTower.algebraMap_smul (Localizations R x.1) r (m.1 x)

Premises used: AlgebraicGeometry.StructureSheaf.Localizations, IsScalarTower.algebraMap_smul, funext, Subtype.val, IsScalarTower.of_algebraMap_smul, 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
X : (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ
⊢ Module
    (Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R R))
      X)
    (Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      X)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U V : Opens (↑(PrimeSpectrum.Top R) : Type u)
i : V ⟶ U
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
x : ↥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.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 V)))
            s) :
        (x : ↥(unop (op V))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
      x =
    (↑s : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) ((i : (a : ↥V) → ↥U) x)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- 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 : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl
x : ↥U
⊢ Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
    ((↑(const f g U hu) : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x :
      Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
    (LocalizedModule.mk f
        (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) g ⋯) :
      LocalizedModule (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl M)

Tactic:
rfl

Premises used: Set.Mem, Quotient.mk', OreLocalization.oreDiv, rfl
-- 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))
⊢ ∃ (g : R) (_ : Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen g) x) (i : basicOpen g ≤ U) (f : 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 g)))
      (const f g (basicOpen g) ⋯)
      ((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.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))))
        s)

Tactic:
⟨g' * g, ?_, ?_, g' • f, Subtype.ext <| funext fun ⟨y, hy⟩ ↦ ?_⟩

Premises used: le_rfl, HMul.hMul, PrimeSpectrum.basicOpen, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.ObjectProperty.FullSubcategory.obj, LE.le.hom, CategoryTheory.Functor.map, funext, Exists.intro, AlgebraicGeometry.StructureSheaf.const, HSMul.hSMul, _private.0.AlgebraicGeometry.StructureSheaf.exists_const.match_1, AlgebraicGeometry.structureSheafInType, Subtype.val, Eq, DFunLike.coe, Subtype.ext
-- 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))
refine_1 : Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen g' ⊓ basicOpen g) x
⊢ Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g' * g)) x

Tactic:
simp only [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
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))
refine_2 : basicOpen g' ⊓ basicOpen g ≤ U
⊢ basicOpen (g' * g) ≤ U

Tactic:
simp only [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
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:
⟨hxg', (hfg ⟨x, hxV⟩).1⟩

Premises used: Set.Mem, setOf, Set.inter, Subtype.mk, And.intro