awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X Y : Scheme
f_1 : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
⊢ Eq (α :=
    (x : ↥X) ×
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
    (Sigma.mk (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
      x
      (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f hf))
    ((fun (f : Spec R ⟶ X) ↦
        (Sigma.mk (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
            (f (closedPoint (↑R : Type u)))
            (Subtype.mk (p := fun (f_2 : X.presheaf.stalk (f (closedPoint (↑R : Type u))) ⟶ R) ↦
              IsLocalHom (R := (↑(X.presheaf.stalk (f (closedPoint (↑R : Type u)))) : Type u)) (S := (↑R : Type u))
                (CommRingCat.Hom.hom f_2))
              (Scheme.stalkClosedPointTo f) ⋯) :
          (x : ↥X) ×
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }))
      ((fun
            (xf :
              (x : ↥X) ×
                { f : X.presheaf.stalk x ⟶ R //
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) ↦
          Spec.map
              (↑(xf.snd (β := fun (x : ↥X) ↦
                    { f : X.presheaf.stalk x ⟶ R //
                      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                        (CommRingCat.Hom.hom f) })) :
                X.presheaf.stalk xf.fst ⟶ R) ≫
            X.fromSpecStalk
              (xf.fst (β := fun (x : ↥X) ↦
                { f : X.presheaf.stalk x ⟶ R //
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })))
        (Sigma.mk (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
          x
          (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f hf))))

Tactic:
SpecToEquivOfLocalRing_eq_iff.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, Exists.intro, AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff
-- 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)
V U : Opens (↑(PrimeSpectrum.Top R) : Type u)
i : V ⟶ U
f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
r : M
s : R
w :
  ∀ (x : ↥U),
    ∃ (hs : s ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      f x =
        LocalizedModule.mk r
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) s hs)
⊢ IsFraction.{u} (R := R) (M := M) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
⟨r, s, fun x => w (i x)⟩

Premises used: Exists.intro, AlgebraicGeometry.StructureSheaf.IsFraction, DFunLike.coe
-- 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)
V U : Opens (↑(PrimeSpectrum.Top R) : Type u)
i : V ⟶ U
f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
r : M
s : R
w :
  ∀ (x : ↥U),
    ∃ (hs : s ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      f x =
        LocalizedModule.mk r
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) s hs)
⊢ IsFraction.{u} (R := R) (M := M) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
exact ⟨r, s, fun x => w (i 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 M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    b
x : ↥U
obtain :
  ∀ (Va : Opens (↑(PrimeSpectrum.Top R) : Type u)) (ma : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va) (ia : Va ⟶ U)
    (ra : M) (sa : R)
    (wa :
      ∀ (x : ↥Va),
        ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
          Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            ((fun (x : ↥Va) ↦
                (a ((ia : (a : ↥Va) → ↥U) x) :
                  Localizations (R := R) M (↑((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 M) (isFractionPrelocal R M) (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 M) (isFractionPrelocal R M) (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 M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    b
x : ↥U
Va : Opens (↑(PrimeSpectrum.Top R) : Type u)
ma : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va
ia : Va ⟶ U
ra : M
sa : R
wa :
  ∀ (x : ↥Va),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥U) x) :
              Localizations (R := R) M (↑((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 : M) (sb : R)
    (wb :
      ∀ (x : ↥Vb),
        ∃ (hs : sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
          Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            ((fun (x : ↥Vb) ↦
                (b ((ib : (a : ↥Vb) → ↥U) x) :
                  Localizations (R := R) M (↑((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 M) (isFractionPrelocal R M) (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 M) (isFractionPrelocal R M) (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 M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    b
x : ↥U
Va : Opens (↑(PrimeSpectrum.Top R) : Type u)
ma : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va
ia : Va ⟶ U
ra : M
sa : R
wa :
  ∀ (x : ↥Va),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥U) x) :
              Localizations (R := R) M (↑((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 : M
sb : R
wb :
  ∀ (x : ↥Vb),
    ∃ (hs : sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Vb) ↦
            (b ((ib : (a : ↥Vb) → ↥U) x) :
              Localizations (R := R) M (↑((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 M) (isFractionPrelocal R M) (U := V) fun (x : ↥V) ↦
      (a + b) ((i : (a : ↥V) → ↥U) x)

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

Premises used: HMul.hMul, HAdd.hAdd, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, HSMul.hSMul, 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 M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    b
x : ↥U
Va : Opens (↑(PrimeSpectrum.Top R) : Type u)
ma : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va
ia : Va ⟶ U
ra : M
sa : R
wa :
  ∀ (x : ↥Va),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥U) x) :
              Localizations (R := R) M (↑((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 : M
sb : R
wb :
  ∀ (x : ↥Vb),
    ∃ (hs : sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Vb) ↦
            (b ((ib : (a : ↥Vb) → ↥U) x) :
              Localizations (R := R) M (↑((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 M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥(Va ⊓ Vb)) ↦ (a + b) ((Va.infLELeft Vb ≫ ia : (a : ↥(Va ⊓ Vb)) → ↥U) x)) x)
        (LocalizedModule.mk (sb • ra + sa • 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 M) (isFractionPrelocal R M) (U := V) fun (x : ↥V) ↦
      (a + b) ((i : (a : ↥V) → ↥U) x)

Tactic:
refine ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, sb • ra + sa • 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 M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
ha :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    a
hb :
  Membership.mem (γ := Set ((x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    b
x_1 : ↥U
Va : Opens (↑(PrimeSpectrum.Top R) : Type u)
ma : (↑x_1 : (↑(PrimeSpectrum.Top R) : Type u)) ∈ Va
ia : Va ⟶ U
ra : M
sa : R
wa :
  ∀ (x : ↥Va),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥U) x) :
              Localizations (R := R) M (↑((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 : M
sb : R
wb :
  ∀ (x : ↥Vb),
    ∃ (hs : sb ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥Vb) ↦
            (b ((ib : (a : ↥Vb) → ↥U) x) :
              Localizations (R := R) M (↑((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)
x y : ↥U
⊢ ∃ (hs : 1 ∉ (↑y : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
    Eq (α := Localizations M (↑y : (↑(PrimeSpectrum.Top R) : Type u)))
      ((fun (x : ↥U) ↦
          (0 ((𝟙 U : (a : ↥U) → ↥U) x) :
            Localizations (R := R) M (↑((𝟙 U : (a : ↥U) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
        y)
      (LocalizedModule.mk 0
        (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑y : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) 1 hs))

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 : R
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))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    a
x : ↥U
obtain :
  ∀ (V : Opens (↑(PrimeSpectrum.Top R) : Type u)) (m : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V) (i : V ⟶ U)
    (ra : M) (sa : R)
    (wa :
      ∀ (x : ↥V),
        ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
          Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            ((fun (x : ↥V) ↦
                (a ((i : (a : ↥V) → ↥U) x) :
                  Localizations (R := R) M (↑((i : (a : ↥V) → ↥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 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, m, i, 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)
r : R
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))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    a
x : ↥U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
m : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V
i : V ⟶ U
ra : M
sa : R
wa :
  ∀ (x : ↥V),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (a ((i : (a : ↥V) → ↥U) x) :
              Localizations (R := R) M (↑((i : (a : ↥V) → ↥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 M) (isFractionPrelocal R M) (U := V) fun (x : ↥V) ↦
      (r • a) ((i : (a : ↥V) → ↥U) x)

Tactic:
⟨V, m, i, r • ra, sa, fun x ↦ ⟨(wa x).1,
      congr(r • $((wa x).2)).trans (LocalizedModule.smul'_mk ..)⟩⟩

Premises used: congrArg, id, LocalizedModule.smul'_mk, Subtype.mk, Exists.intro, HSMul.hSMul, Eq.trans
-- 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
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))))
    {f : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)) |
      PrelocalPredicate.pred (T := Localizations M)
        (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) f}
    a
x : ↥U
V : Opens (↑(PrimeSpectrum.Top R) : Type u)
m : (↑x : (↑(PrimeSpectrum.Top R) : Type u)) ∈ V
i : V ⟶ U
ra : M
sa : R
wa :
  ∀ (x : ↥V),
    ∃ (hs : sa ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥V) ↦
            (a ((i : (a : ↥V) → ↥U) x) :
              Localizations (R := R) M (↑((i : (a : ↥V) → ↥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 M) (isFractionPrelocal R M) (U := V) fun (x : ↥V) ↦
      (r • a) ((i : (a : ↥V) → ↥U) x)

Tactic:
exact ⟨V, m, i, r • ra, sa, fun x ↦ ⟨(wa x).1,
      congr(r • $((wa x).2)).trans (LocalizedModule.smul'_mk ..)⟩⟩