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)
a b : (x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule A U)))) a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule A U)))) b
x : ↥U
obtain :
  ∀ (Va : Opens (↑(PrimeSpectrum.Top R) : Type u)) (ma : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va) (ia : Va ⟶ U)
    (ra : A) (sa : R)
    (wa :
      ∀ (x : ↥Va),
        ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
          Eq (α := Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            ((fun (x : ↥Va) ↦
                (a ((ia : (a : ↥Va) → ↥U) x) :
                  Localizations (R := R) A (↑((ia : (a : ↥Va) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
              x)
            (LocalizedModule.mk ra
              (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sa
                hs))),
    ∃ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (_ : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U),
      PrelocalPredicate.pred (T := Localizations A) (isFractionPrelocal R A) (U := V) fun (x : ↥V) ↦
        (a * b) ((i : (a : ↥V) → ↥U) x)
⊢ ∃ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (_ : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U),
    PrelocalPredicate.pred (T := Localizations A) (isFractionPrelocal R A) (U := V) fun (x : ↥V) ↦
      (a * b) ((i : (a : ↥V) → ↥U) x)

Tactic:
obtain ⟨Va, ma, ia, ra, sa, wa⟩ := ha 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
P : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
a b : (x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule A U)))) a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule A U)))) b
x : ↥U
Va : Opens (↑(PrimeSpectrum.Top R) : Type u)
ma : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va
ia : Va ⟶ U
ra : A
sa : R
wa :
  ∀ (x : ↥Va),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥U) x) :
              Localizations (R := R) A (↑((ia : (a : ↥Va) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk ra
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sa hs))
obtain :
  ∀ (Vb : Opens (↑(PrimeSpectrum.Top R) : Type u)) (mb : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Vb) (ib : Vb ⟶ U)
    (rb : A) (sb : R)
    (wb :
      ∀ (x : ↥Vb),
        ∃ (hs : sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
          Eq (α := Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            ((fun (x : ↥Vb) ↦
                (b ((ib : (a : ↥Vb) → ↥U) x) :
                  Localizations (R := R) A (↑((ib : (a : ↥Vb) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
              x)
            (LocalizedModule.mk rb
              (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sb
                hs))),
    ∃ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (_ : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U),
      PrelocalPredicate.pred (T := Localizations A) (isFractionPrelocal R A) (U := V) fun (x : ↥V) ↦
        (a * b) ((i : (a : ↥V) → ↥U) x)
⊢ ∃ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (_ : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U),
    PrelocalPredicate.pred (T := Localizations A) (isFractionPrelocal R A) (U := V) fun (x : ↥V) ↦
      (a * b) ((i : (a : ↥V) → ↥U) x)

Tactic:
obtain ⟨Vb, mb, ib, rb, sb, wb⟩ := hb 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
P : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
a b : (x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule A U)))) a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule A U)))) b
x : ↥U
Va : Opens (↑(PrimeSpectrum.Top R) : Type u)
ma : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va
ia : Va ⟶ U
ra : A
sa : R
wa :
  ∀ (x : ↥Va),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥U) x) :
              Localizations (R := R) A (↑((ia : (a : ↥Va) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk ra
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sa hs))
Vb : Opens (↑(PrimeSpectrum.Top R) : Type u)
mb : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Vb
ib : Vb ⟶ U
rb : A
sb : R
wb :
  ∀ (x : ↥Vb),
    ∃ (hs : sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Vb) ↦
            (b ((ib : (a : ↥Vb) → ↥U) x) :
              Localizations (R := R) A (↑((ib : (a : ↥Vb) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk rb
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sb hs))
⊢ ∃ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (_ : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U),
    PrelocalPredicate.pred (T := Localizations A) (isFractionPrelocal R A) (U := V) fun (x : ↥V) ↦
      (a * b) ((i : (a : ↥V) → ↥U) x)

Tactic:
⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ra * rb, sa * sb, fun x ↦ ?_⟩

Premises used: HMul.hMul, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, TopologicalSpace.Opens.infLELeft, Min.min
-- 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)
a b : (x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule A U)))) a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule A U)))) b
x : ↥U
Va : Opens (↑(PrimeSpectrum.Top R) : Type u)
ma : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va
ia : Va ⟶ U
ra : A
sa : R
wa :
  ∀ (x : ↥Va),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥U) x) :
              Localizations (R := R) A (↑((ia : (a : ↥Va) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk ra
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sa hs))
Vb : Opens (↑(PrimeSpectrum.Top R) : Type u)
mb : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Vb
ib : Vb ⟶ U
rb : A
sb : R
wb :
  ∀ (x : ↥Vb),
    ∃ (hs : sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Vb) ↦
            (b ((ib : (a : ↥Vb) → ↥U) x) :
              Localizations (R := R) A (↑((ib : (a : ↥Vb) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk rb
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sb hs))
refine :
  ∀ (x : ↥(Va ⊓ Vb)),
    ∃ (hs : sa * sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥(Va ⊓ Vb)) ↦ (a * b) ((Va.infLELeft Vb ≫ ia : (a : ↥(Va ⊓ Vb)) → ↥U) x)) x)
        (LocalizedModule.mk (ra * rb)
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) (sa * sb)
            hs))
⊢ ∃ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (_ : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U),
    PrelocalPredicate.pred (T := Localizations A) (isFractionPrelocal R A) (U := V) fun (x : ↥V) ↦
      (a * b) ((i : (a : ↥V) → ↥U) x)

Tactic:
refine ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ra * rb, sa * sb, fun 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
P : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
a b : (x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule A U)))) a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule A U)))) b
x_1 : ↥U
Va : Opens (↑(PrimeSpectrum.Top R) : Type u)
ma : (↑x_1 : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va
ia : Va ⟶ U
ra : A
sa : R
wa :
  ∀ (x : ↥Va),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥U) x) :
              Localizations (R := R) A (↑((ia : (a : ↥Va) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk ra
          (Subtype.mk (p := fun (x_2 : R) ↦ x_2 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sa hs))
Vb : Opens (↑(PrimeSpectrum.Top R) : Type u)
mb : (↑x_1 : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Vb
ib : Vb ⟶ U
rb : A
sb : R
wb :
  ∀ (x : ↥Vb),
    ∃ (hs : sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Vb) ↦
            (b ((ib : (a : ↥Vb) → ↥U) x) :
              Localizations (R := R) A (↑((ib : (a : ↥Vb) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk rb
          (Subtype.mk (p := fun (x_2 : R) ↦ x_2 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sb hs))
x : ↥(Va ⊓ Vb)
⊢ sa ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Va) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal

Tactic:
obtain ⟨hsax, hsa⟩ := wa ⟨x.1, x.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)
a b : (x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule A U)))) a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (sectionsSubmodule A U)))) b
x_1 : ↥U
Va : Opens (↑(PrimeSpectrum.Top R) : Type u)
ma : (↑x_1 : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va
ia : Va ⟶ U
ra : A
sa : R
wa :
  ∀ (x : ↥Va),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥U) x) :
              Localizations (R := R) A (↑((ia : (a : ↥Va) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk ra
          (Subtype.mk (p := fun (x_2 : R) ↦ x_2 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sa hs))
Vb : Opens (↑(PrimeSpectrum.Top R) : Type u)
mb : (↑x_1 : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Vb
ib : Vb ⟶ U
rb : A
sb : R
wb :
  ∀ (x : ↥Vb),
    ∃ (hs : sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations A (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Vb) ↦
            (b ((ib : (a : ↥Vb) → ↥U) x) :
              Localizations (R := R) A (↑((ib : (a : ↥Vb) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk rb
          (Subtype.mk (p := fun (x_2 : R) ↦ x_2 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) sb hs))
x : ↥(Va ⊓ Vb)
hsax :
  sa ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Va) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal
⊢ Eq (α :=
    Localizations A
      (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Va) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
            ⋯) :
        (↑(PrimeSpectrum.Top R) : Type u)))
    ((fun (x : ↥Va) ↦
        (a ((ia : (a : ↥Va) → ↥U) x) :
          Localizations (R := R) A (↑((ia : (a : ↥Va) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
      (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Va) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
        ⋯))
    (LocalizedModule.mk ra
      (Subtype.mk (p := fun (x_2 : R) ↦
        x_2 ∈
          (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ Va)
                    (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ⋯) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        sa hsax))

Tactic:
obtain ⟨hsax, hsa⟩ := wa ⟨x.1, x.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 : R
x y : ↥U
⊢ 1 ∉ (↑y : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal

Tactic:
simp [Ideal.IsPrime.one_notMem]

Premises used: Ideal.IsPrime.one_notMem
-- 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 :
  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
obtain :
  ∀ (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))),
    ∃ (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)
⊢ ∃ (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:
obtain ⟨V, hxV, hVU, rx, rs, hr⟩ := r.2 x

Premises used: 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 :
  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))
obtain :
  ∀ (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))),
    ∃ (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)
⊢ ∃ (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:
obtain ⟨W, hxW, hWU, ax, as, ha⟩ := ha 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
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))
⊢ ∃ (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:
⟨V ⊓ W, ⟨hxV, hxW⟩, homOfLE (inf_le_left.trans hVU.le), rx • ax, as * rs, fun y ↦ ?_⟩

Premises used: HMul.hMul, Quiver.Hom.le, CategoryTheory.homOfLE, And.intro, Exists.intro, HSMul.hSMul, inf_le_left, LE.le.trans, Min.min