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
s : R
f : M
n : ℕ
⊢ 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 s)))
    (const f 1 (basicOpen s) ⋯) (const (s ^ n • f) (s ^ n) (basicOpen s) ⋯)

Tactic:
exact const_eq_const_of_smul_eq_smul (H := by simp) ..

Premises used: AlgebraicGeometry.StructureSheaf.const_eq_const_of_smul_eq_smul
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    ((toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        (LocalizedModule.mk a b) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f)))
    ((toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        (LocalizedModule.mk c d) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f)))
this : Membership.mem (γ := Ideal R) (Ideal.radical (Submodule.colon (M := M) ⊥ {d • a - b • c})) f
rw : ∃ (u : ↥(Submonoid.powers f)), u • d • a = u • b • c
⊢ Eq (α := LocalizedModule.Away f M) (LocalizedModule.mk a b) (LocalizedModule.mk c d)

Tactic:
rw [LocalizedModule.mk_eq]

Premises used: LocalizedModule.mk_eq
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    ((toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        (LocalizedModule.mk a b) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f)))
    ((toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        (LocalizedModule.mk c d) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f)))
this : Membership.mem (γ := Ideal R) (Ideal.radical (Submodule.colon (M := M) ⊥ {d • a - b • c})) f
obtain :
  ∀ (n : ℕ) (hn : Membership.mem (γ := Ideal R) (Submodule.colon (M := M) ⊥ {d • a - b • c}) (f ^ n)),
    ∃ (u : ↥(Submonoid.powers f)), u • d • a = u • b • c
⊢ ∃ (u : ↥(Submonoid.powers f)), u • d • a = u • b • c

Tactic:
obtain ⟨n, hn⟩ := this
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    ((toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        (LocalizedModule.mk a b) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f)))
    ((toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        (LocalizedModule.mk c d) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f)))
n : ℕ
hn : Membership.mem (γ := Ideal R) (Submodule.colon (M := M) ⊥ {d • a - b • c}) (f ^ n)
⊢ HSMul.hSMul (α := ↥(Submonoid.powers f))
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers f) x) (f ^ n) ⋯) (d • a) =
    HSMul.hSMul (α := ↥(Submonoid.powers f))
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers f) x) (f ^ n) ⋯) (b • c)

Tactic:
simpa [sub_eq_zero, smul_sub] using Submodule.mem_colon.mp hn _ rfl

Premises used: sub_eq_zero, smul_sub, Iff.mp, Submodule.mem_colon, rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    ((toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        (LocalizedModule.mk a b) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f)))
    ((toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        (LocalizedModule.mk c d) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f)))
n : ℕ
hn : Membership.mem (γ := Ideal R) (Submodule.colon (M := M) ⊥ {d • a - b • c}) (f ^ n)
⊢ ∃ (u : ↥(Submonoid.powers f)), u • d • a = u • b • c

Tactic:
exact ⟨⟨f ^ n, n, rfl⟩, by simpa [sub_eq_zero, smul_sub] using Submodule.mem_colon.mp hn _ rfl⟩
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    ((toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        (LocalizedModule.mk a b) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f)))
    ((toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        (LocalizedModule.mk c d) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f)))
h : Membership.mem (γ := Ideal R) (Ideal.radical (Submodule.colon (M := M) ⊥ {d • a - b • c})) f
⊢ Eq (α := LocalizedModule.Away f M) (LocalizedModule.mk a b) (LocalizedModule.mk c d)

Tactic:
suffices f ∈ ((⊥ : Submodule R M).colon {d • a - b • c}).radical by
    rw [LocalizedModule.mk_eq]
    obtain ⟨n, hn⟩ := this
    exact ⟨⟨f ^ n, n, rfl⟩, by simpa [sub_eq_zero, smul_sub] using Submodule.mem_colon.mp hn _ rfl⟩
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    ((toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        (LocalizedModule.mk a b) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f)))
    ((toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
        (LocalizedModule.mk c d) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f)))
⊢ Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    (const a (↑b : R) (basicOpen f) ⋯) (const c (↑d : R) (basicOpen f) ⋯)

Tactic:
simp only [toBasicOpenₗ_mk] at h_eq

Premises used: _private.0.AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_mk
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    (const a (↑b : R) (basicOpen f) ⋯) (const c (↑d : R) (basicOpen f) ⋯)
h :
  ∀ (x : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R))
        (PrimeSpectrum.zeroLocus (↑(Submodule.colon (M := M) ⊥ {d • a - b • c}) : Set R)) x →
      f ∈ x.asIdeal
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (Submodule.colon (M := M) ⊥ {d • a - b • c})) f

Tactic:
rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.mem_vanishingIdeal]

Premises used: PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.mem_vanishingIdeal
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    (const a (↑b : R) (basicOpen f) ⋯) (const c (↑d : R) (basicOpen f) ⋯)
p : PrimeSpectrum R
hfp :
  Membership.mem (γ := Set (PrimeSpectrum R))
    (PrimeSpectrum.zeroLocus (↑(Submodule.colon (M := M) ⊥ {d • a - b • c}) : Set R)) p
h : ∀ (hfp : f ∉ p.asIdeal), p ∉ PrimeSpectrum.zeroLocus (↑(Submodule.colon (M := M) ⊥ {d • a - b • c}) : Set R)
⊢ f ∈ p.asIdeal

Tactic:
contrapose hfp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    (const a (↑b : R) (basicOpen f) ⋯) (const c (↑d : R) (basicOpen f) ⋯)
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
h :
  ∀
    (u :
      ↥(↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                  Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p hfp) :
              (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
    (hu :
      u •
          HSMul.hSMul (α :=
            ↥(↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                        Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p
                        hfp) :
                    (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
            (Subtype.mk (p := fun (x : R) ↦
              x ∈
                (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                          Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p
                          hfp) :
                      (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
              (↑d : R) ⋯)
            a =
        u •
          HSMul.hSMul (α :=
            ↥(↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                        Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p
                        hfp) :
                    (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
            (Subtype.mk (p := fun (x : R) ↦
              x ∈
                (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                          Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p
                          hfp) :
                      (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
              (↑b : R) ⋯)
            c),
    p ∉ PrimeSpectrum.zeroLocus (↑(Submodule.colon (M := M) ⊥ {d • a - b • c}) : Set R)
⊢ p ∉ PrimeSpectrum.zeroLocus (↑(Submodule.colon (M := M) ⊥ {d • a - b • c}) : Set R)

Tactic:
obtain ⟨u, hu⟩ := LocalizedModule.mk_eq.mp congr(($h_eq).1 ⟨p, hfp⟩)

Premises used: congrArg, LocalizedModule.mk_eq, id, Subtype.mk, Iff.mp, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    (const a (↑b : R) (basicOpen f) ⋯) (const c (↑d : R) (basicOpen f) ⋯)
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
u :
  ↥(↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
              Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p hfp) :
          (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl
hu :
  u •
      HSMul.hSMul (α :=
        ↥(↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                    Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p hfp) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        (Subtype.mk (p := fun (x : R) ↦
          x ∈
            (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                      Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p
                      hfp) :
                  (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
          (↑d : R) ⋯)
        a =
    u •
      HSMul.hSMul (α :=
        ↥(↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                    Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p hfp) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        (Subtype.mk (p := fun (x : R) ↦
          x ∈
            (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                      Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p
                      hfp) :
                  (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
          (↑b : R) ⋯)
        c
h : ∃ a_1 ∈ (↑(Submodule.colon (M := M) ⊥ {d • a - b • c}) : Set R), a_1 ∉ (↑p.asIdeal : Set R)
⊢ p ∉ PrimeSpectrum.zeroLocus (↑(Submodule.colon (M := M) ⊥ {d • a - b • c}) : Set R)

Tactic:
rw [PrimeSpectrum.mem_zeroLocus, Set.not_subset]

Premises used: PrimeSpectrum.mem_zeroLocus, Set.not_subset
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    (const a (↑b : R) (basicOpen f) ⋯) (const c (↑d : R) (basicOpen f) ⋯)
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
u :
  ↥(↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
              Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p hfp) :
          (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl
hu :
  u •
      HSMul.hSMul (α :=
        ↥(↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                    Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p hfp) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        (Subtype.mk (p := fun (x : R) ↦
          x ∈
            (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                      Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p
                      hfp) :
                  (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
          (↑d : R) ⋯)
        a =
    u •
      HSMul.hSMul (α :=
        ↥(↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                    Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p hfp) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        (Subtype.mk (p := fun (x : R) ↦
          x ∈
            (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                      Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p
                      hfp) :
                  (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
          (↑b : R) ⋯)
        c
⊢ (↑u : R) ∈ (↑(Submodule.colon (M := M) ⊥ {d • a - b • c}) : Set R)

Tactic:
simpa [sub_eq_zero, smul_sub]

Premises used: sub_eq_zero, smul_sub
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen f)))
    (const a (↑b : R) (basicOpen f) ⋯) (const c (↑d : R) (basicOpen f) ⋯)
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
u :
  ↥(↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
              Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p hfp) :
          (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl
hu :
  u •
      HSMul.hSMul (α :=
        ↥(↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                    Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p hfp) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        (Subtype.mk (p := fun (x : R) ↦
          x ∈
            (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                      Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p
                      hfp) :
                  (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
          (↑d : R) ⋯)
        a =
    u •
      HSMul.hSMul (α :=
        ↥(↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                    Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p hfp) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        (Subtype.mk (p := fun (x : R) ↦
          x ∈
            (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦
                      Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) (unop (op (basicOpen f))) x) p
                      hfp) :
                  (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
          (↑b : R) ⋯)
        c
⊢ ∃ a_1 ∈ (↑(Submodule.colon (M := M) ⊥ {d • a - b • c}) : Set R), a_1 ∉ (↑p.asIdeal : Set R)

Tactic:
exact ⟨u.1, by simpa [sub_eq_zero, smul_sub], u.2⟩