awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
T : Type u
inst : CommRing T
inst_1 : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ Eq (α := Ideal T) (PrimeSpectrum.asIdeal (PrimeSpectrum.comap (S := ResidueField T) (residue T) ⊥))
    (PrimeSpectrum.asIdeal (closedPoint T))

Tactic:
Ideal.mk_ker

Premises used: IsLocalRing.maximalIdeal, IsLocalRing.ResidueField, Ideal.comap, Ideal.mk_ker, RingHom.ker
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
T : Type u
inst : CommRing T
inst_1 : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ Eq (α := Ideal T) (PrimeSpectrum.asIdeal (PrimeSpectrum.comap (S := ResidueField T) (residue T) ⊥))
    (PrimeSpectrum.asIdeal (closedPoint T))

Tactic:
exact Ideal.mk_ker

Premises used: Ideal.mk_ker
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
rw : Ideal.IsMaximal (PrimeSpectrum.asIdeal { asIdeal := maximalIdeal R, isPrime := ⋯ })
⊢ IsClosed (X := PrimeSpectrum R) {closedPoint R}

Tactic:
rw [PrimeSpectrum.isClosed_singleton_iff_isMaximal, closedPoint]

Premises used: PrimeSpectrum.isClosed_singleton_iff_isMaximal, IsLocalRing.closedPoint
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
⊢ Ideal.IsMaximal (PrimeSpectrum.asIdeal { asIdeal := maximalIdeal R, isPrime := ⋯ })

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : Ring.KrullDimLE 1 R
x : PrimeSpectrum R
⊢ x = ⊥ ∨ x = ⊤

Tactic:
Order.krullDim_le_one_iff_of_boundedOrder.mp Order.KrullDimLE.krullDim_le _

Premises used: Order.krullDim_le_one_iff_of_boundedOrder, Iff.mp, Order.KrullDimLE.krullDim_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ topologicalKrullDim.{u} (PrimeSpectrum R) = ringKrullDim R

Tactic:
Order.krullDim_orderDual.symm.trans <| Order.krullDim_eq_of_orderIso
  (PrimeSpectrum.pointsEquivIrreducibleCloseds R).symm

Premises used: PrimeSpectrum.pointsEquivIrreducibleCloseds, Order.krullDim_eq_of_orderIso, OrderIso.symm, topologicalKrullDim, Order.krullDim_orderDual, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
e : R
he : IsIdempotentElem e
⊢ e * (1 - e) = 0

Tactic:
simp [mul_sub, he.eq]

Premises used: mul_sub, IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
e : R
he : IsIdempotentElem e
⊢ e + (1 - e) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
e : R
he : IsIdempotentElem e
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus {e}) (zeroLocus {1 - (1 - e)})
rw₁ rw₂ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus {e}) (zeroLocus {e})
⊢ zeroLocus {e} = (↑(basicOpen (1 - e)) : Set (PrimeSpectrum R))

Tactic:
rw [basicOpen_eq_zeroLocus_of_isIdempotentElem _ he.one_sub, sub_sub_cancel]

Premises used: IsIdempotentElem.one_sub, PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem, sub_sub_cancel
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
s : Set (PrimeSpectrum R)
⊢ IsClopen s ↔ ∃ (e : R), IsIdempotentElem e ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
⟨exists_idempotent_basicOpen_eq_of_isClopen, ?_⟩

Premises used: PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen, Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
s : Set (PrimeSpectrum R)
refine : (∃ (e : R), IsIdempotentElem e ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))) → IsClopen s
⊢ IsClopen s ↔ ∃ (e : R), IsIdempotentElem e ∧ s = (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
refine ⟨exists_idempotent_basicOpen_eq_of_isClopen, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClopen (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
⟨?_, (basicOpen e).2⟩

Premises used: PrimeSpectrum.basicOpen, And.intro, TopologicalSpace.Opens.is_open', IsClopen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
e : R
he : IsIdempotentElem e
refine : IsClosed (↑(basicOpen e) : Set (PrimeSpectrum R))
⊢ IsClopen (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
refine ⟨?_, (basicOpen e).2⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
e : R
he : IsIdempotentElem e
rw : IsClosed (X := PrimeSpectrum R) (zeroLocus {1 - e})
⊢ IsClosed (↑(basicOpen e) : Set (PrimeSpectrum R))

Tactic:
rw [PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem e he]

Premises used: PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClosed (X := PrimeSpectrum R) (zeroLocus {1 - e})

Tactic:
isClosed_zeroLocus _

Premises used: PrimeSpectrum.isClosed_zeroLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
e : R
he : IsIdempotentElem e
⊢ IsClosed (X := PrimeSpectrum R) (zeroLocus {1 - e})

Tactic:
exact isClosed_zeroLocus _

Premises used: PrimeSpectrum.isClosed_zeroLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
s : Set (PrimeSpectrum R)
⊢ IsClopen s ↔ ∃ (e : R), IsIdempotentElem e ∧ s = zeroLocus {e}

Tactic:
isClopen_iff.trans <| ⟨fun ⟨e, he, h⟩ ↦ ⟨1 - e, he.one_sub,
    h.trans (basicOpen_eq_zeroLocus_of_isIdempotentElem e he)⟩,
    fun ⟨e, he, h⟩ ↦ ⟨1 - e, he.one_sub, h.trans (zeroLocus_eq_basicOpen_of_isIdempotentElem e he)⟩⟩

Premises used: IsIdempotentElem.one_sub, PrimeSpectrum.zeroLocus, PrimeSpectrum.basicOpen, PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem, PrimeSpectrum.zeroLocus_eq_basicOpen_of_isIdempotentElem, HSub.hSub, _private.0.PrimeSpectrum.isClopen_iff_zeroLocus.match_2, Exists, PrimeSpectrum.isClopen_iff, And, IsIdempotentElem, SetLike.coe, _private.0.PrimeSpectrum.isClopen_iff_zeroLocus.match_1, And.intro, Iff.intro, Exists.intro, Iff.trans, Singleton.singleton, OfNat.ofNat, Eq, Eq.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
s : Clopens (PrimeSpectrum R)
⊢ basicOpen
      (↑((OrderIso.symm isIdempotentElemEquivClopens :
              (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e })
            s) :
        R) =
    s.toOpens

Tactic:
Opens.ext <| congr_arg (·.1) (isIdempotentElemEquivClopens.apply_symm_apply s)

Premises used: TopologicalSpace.Opens.ext
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
e : { e : R // IsIdempotentElem e }
⊢ (↑((isIdempotentElemEquivClopens : (a : { e : R // IsIdempotentElem e }) → Clopens (PrimeSpectrum R)) e :
          Clopens (PrimeSpectrum R)) :
      Set (PrimeSpectrum R)) =
    (↑(basicOpen (↑e : R)) : Set (PrimeSpectrum R))

Tactic:
rfl

Premises used: Set.Mem, setOf, Not, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
e : { e : R // IsIdempotentElem e }
⊢ Eq (α := Opens (PrimeSpectrum R))
    (Clopens.toOpens
      ((isIdempotentElemEquivClopens : (a : { e : R // IsIdempotentElem e }) → Clopens (PrimeSpectrum R)) e))
    (basicOpen (↑e : R))

Tactic:
rfl

Premises used: PrimeSpectrum.basicOpen, Set.Mem, TopologicalSpace.Clopens.toOpens, setOf, Not, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
e₁ e₂ : (↑{e : R | IsIdempotentElem e} : Type u)
⊢ Eq (α := Clopens (PrimeSpectrum R))
    ((isIdempotentElemEquivClopens : (a : { e : R // IsIdempotentElem e }) → Clopens (PrimeSpectrum R))
        (Subtype.mk (p := fun (e : R) ↦ IsIdempotentElem e) ((↑e₁ : R) * (↑e₂ : R)) ⋯) :
      Clopens (PrimeSpectrum R))
    ((isIdempotentElemEquivClopens : (a : { e : R // IsIdempotentElem e }) → Clopens (PrimeSpectrum R)) e₁ ⊓
        (isIdempotentElemEquivClopens : (a : { e : R // IsIdempotentElem e }) → Clopens (PrimeSpectrum R)) e₂ :
      Clopens (PrimeSpectrum R))

Tactic:
map_inf ..

Premises used: InfHomClass.map_inf
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
e : (↑{e : R | IsIdempotentElem e} : Type u)
⊢ Eq (α := Clopens (PrimeSpectrum R))
    ((isIdempotentElemEquivClopens : (a : { e : R // IsIdempotentElem e }) → Clopens (PrimeSpectrum R))
        (Subtype.mk (p := fun (e : R) ↦ IsIdempotentElem e) (1 - (↑e : R)) ⋯) :
      Clopens (PrimeSpectrum R))
    (((isIdempotentElemEquivClopens : (a : { e : R // IsIdempotentElem e }) → Clopens (PrimeSpectrum R)) e)ᶜ :
      Clopens (PrimeSpectrum R))

Tactic:
map_compl ..

Premises used: map_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
s₁ s₂ : Clopens (PrimeSpectrum R)
⊢ (OrderIso.symm isIdempotentElemEquivClopens : (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e })
      (s₁ ⊓ s₂) =
    Subtype.mk (p := fun (e : R) ↦ IsIdempotentElem e)
      (HMul.hMul (α := R)
        (↑((OrderIso.symm isIdempotentElemEquivClopens :
                (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e })
              s₁) :
          R)
        (↑((OrderIso.symm isIdempotentElemEquivClopens :
                (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e })
              s₂) :
          R))
      ⋯

Tactic:
map_inf ..

Premises used: InfHomClass.map_inf
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
s : Clopens (PrimeSpectrum R)
⊢ (OrderIso.symm isIdempotentElemEquivClopens : (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e }) sᶜ =
    Subtype.mk (p := fun (e : R) ↦ IsIdempotentElem e)
      (HSub.hSub (α := R) 1
        (↑((OrderIso.symm isIdempotentElemEquivClopens :
                (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e })
              s) :
          R))
      ⋯

Tactic:
map_compl ..

Premises used: map_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
⊢ Eq.{u + 1} (α := { e : R // IsIdempotentElem e })
    ((OrderIso.symm isIdempotentElemEquivClopens : (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e })
        ⊤ :
      { e : R // IsIdempotentElem e })
    (Subtype.mk (p := fun (e : R) ↦ IsIdempotentElem e) 1 ⋯ : { e : R // IsIdempotentElem e })

Tactic:
map_top _

Premises used: TopHomClass.map_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
⊢ Eq.{u + 1} (α := { e : R // IsIdempotentElem e })
    ((OrderIso.symm isIdempotentElemEquivClopens : (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e })
        ⊥ :
      { e : R // IsIdempotentElem e })
    (Subtype.mk (p := fun (e : R) ↦ IsIdempotentElem e) 0 ⋯ : { e : R // IsIdempotentElem e })

Tactic:
map_bot _

Premises used: BotHomClass.map_bot
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
s₁ s₂ : Clopens (PrimeSpectrum R)
⊢ (OrderIso.symm isIdempotentElemEquivClopens : (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e })
      (s₁ ⊔ s₂) =
    Subtype.mk (p := fun (e : R) ↦ IsIdempotentElem e)
      (HAdd.hAdd (α := R)
          (↑((OrderIso.symm isIdempotentElemEquivClopens :
                  (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e })
                s₁) :
            R)
          (↑((OrderIso.symm isIdempotentElemEquivClopens :
                  (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e })
                s₂) :
            R) -
        HMul.hMul (α := R)
          (↑((OrderIso.symm isIdempotentElemEquivClopens :
                  (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e })
                s₁) :
            R)
          (↑((OrderIso.symm isIdempotentElemEquivClopens :
                  (a : Clopens (PrimeSpectrum R)) → { e : R // IsIdempotentElem e })
                s₂) :
            R))
      ⋯

Tactic:
map_sup ..

Premises used: SupHomClass.map_sup
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ Nontrivial (LocalizedModule p.asIdeal.primeCompl M)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Module.support
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
⊢ p ∉ support R M ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl M)

Tactic:
not_nontrivial_iff_subsingleton

Premises used: Set.Mem, setOf, not_nontrivial_iff_subsingleton, Module.support
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
⊢ p ∉ support R M ↔ ∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0

Tactic:
simp only [notMem_support_iff, Ideal.primeCompl, LocalizedModule.subsingleton_iff,
    Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_compl_iff, SetLike.mem_coe]

Premises used: Subsemigroup.mem_mk, LocalizedModule.subsingleton_iff, Submonoid.mem_mk, SetLike.mem_coe, Module.notMem_support_iff, Ideal.primeCompl, Set.mem_compl_iff
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
rw : (¬∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0) ↔ ∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ ∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0

Tactic:
rw [← @not_not (_ ∈ _), notMem_support_iff']

Premises used: Classical.not_not, Module.notMem_support_iff'
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
push : (∃ (m : M), ∀ (r : R) (_ : r ∉ p.asIdeal), r • m ≠ 0) ↔ ∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0
⊢ (¬∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0) ↔ ∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
⊢ (∃ (m : M), ∀ (r : R) (_ : r ∉ p.asIdeal), r • m ≠ 0) ↔ ∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
rw : (∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
    ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal

Tactic:
rw [Module.mem_support_iff']

Premises used: Module.mem_support_iff'
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
simp_rw :
  (∃ (m : M), ∀ (r : R), r • m = 0 → r ∈ p.asIdeal) ↔ ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
simp_rw₁ :
  (∃ (m : M), ∀ (r : R), r • m = 0 → r ∈ p.asIdeal) ↔
    ∃ (m : M), ∀ ⦃x : R⦄, Membership.mem (γ := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) x → x ∈ p.asIdeal
⊢ (∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal

Tactic:
simp_rw [not_imp_not, SetLike.le_def, Submodule.mem_annihilator_span_singleton]

Premises used: SetLike.le_def, Submodule.mem_annihilator_span_singleton, not_imp_not
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p q : PrimeSpectrum R
H : p ≤ q
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p
rw :
  ∀ (hp : ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal),
    ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ q.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) q

Tactic:
rw [Module.mem_support_iff_exists_annihilator] at hp ⊢

Premises used: Module.mem_support_iff_exists_annihilator
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p q : PrimeSpectrum R
H : p ≤ q
hp : ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
⊢ ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ q.asIdeal

Tactic:
⟨_, hp.choose_spec.trans H⟩

Premises used: Exists.choose_spec, Exists.intro, LE.le.trans
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p q : PrimeSpectrum R
H : p ≤ q
hp : ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
⊢ ∃ (m : M), Submodule.annihilator (M := M) (R ∙ m) ≤ q.asIdeal

Tactic:
exact ⟨_, hp.choose_spec.trans H⟩
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
mp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p →
    ∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
mpr :
  (∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal) →
    Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
    ∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal

Tactic:
constructor
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
mp : (¬∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal) → p ∉ support R M
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p →
    ∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal

Tactic:
contrapose
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
mp :
  (¬∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal) →
    ∀ x ∈ s, x ∈ (↑(LinearMap.ker (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)) : Set M)
⊢ (¬∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal) → p ∉ support R M

Tactic:
rw [notMem_support_iff, LocalizedModule.subsingleton_iff_ker_eq_top, ← top_le_iff,
      ← hs, Submodule.span_le, Set.subset_def]

Premises used: Set.subset_def, LocalizedModule.subsingleton_iff_ker_eq_top, Module.notMem_support_iff, top_le_iff, Submodule.span_le
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
mp : (¬∃ m ∈ s, ∀ ⦃x : R⦄, x • m = 0 → x ∈ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0
⊢ (¬∃ m ∈ s, Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal) →
    ∀ x ∈ s, x ∈ (↑(LinearMap.ker (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)) : Set M)

Tactic:
simp_rw [SetLike.le_def, Submodule.mem_annihilator_span_singleton, SetLike.mem_coe,
      LocalizedModule.mem_ker_mkLinearMap_iff]

Premises used: LocalizedModule.mem_ker_mkLinearMap_iff, SetLike.le_def, SetLike.mem_coe, Submodule.mem_annihilator_span_singleton
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
mp : (∀ (m : M) (_ : m ∈ s), ∃ (x : R), x • m = 0 ∧ x ∉ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0
⊢ (¬∃ m ∈ s, ∀ ⦃x : R⦄, x • m = 0 → x ∈ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
mp : (∀ (m : M) (_ : m ∈ s), ∃ x ∉ p.asIdeal, x • m = 0) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0
⊢ (∀ (m : M) (_ : m ∈ s), ∃ (x : R), x • m = 0 ∧ x ∉ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0

Tactic:
simp_rw [and_comm]

Premises used: and_comm
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
⊢ (∀ (m : M) (_ : m ∈ s), ∃ x ∉ p.asIdeal, x • m = 0) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0

Tactic:
id

Premises used: Set.Mem, setOf, id, Not
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
⊢ (∀ (m : M) (_ : m ∈ s), ∃ x ∉ p.asIdeal, x • m = 0) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0

Tactic:
exact id

Premises used: id
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
m : M
left : m ∈ s
hm : Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p

Tactic:
mem_support_iff_exists_annihilator.mpr ⟨m, hm⟩

Premises used: Iff.mpr, Module.mem_support_iff_exists_annihilator, Exists.intro
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
s : Set M
hs : Eq (α := Submodule R M) (Submodule.span R s) ⊤
m : M
left : m ∈ s
hm : Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p

Tactic:
exact mem_support_iff_exists_annihilator.mpr ⟨m, hm⟩

Premises used: Iff.mpr, Module.mem_support_iff_exists_annihilator, Exists.intro
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p
obtain : ∀ (m : M) (hm : Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal), annihilator R M ≤ p.asIdeal
⊢ annihilator R M ≤ p.asIdeal

Tactic:
obtain ⟨m, hm⟩ := mem_support_iff_exists_annihilator.mp hp

Premises used: Module.mem_support_iff_exists_annihilator, Iff.mp
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p
m : M
hm : Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
⊢ annihilator R M ≤ p.asIdeal

Tactic:
le_trans ((Submodule.subtype _).annihilator_le_of_injective Subtype.val_injective) hm

Premises used: Subtype.val_injective, LinearMap.annihilator_le_of_injective, Submodule.subtype, le_trans
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p
m : M
hm : Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
⊢ annihilator R M ≤ p.asIdeal

Tactic:
exact le_trans ((Submodule.subtype _).annihilator_le_of_injective Subtype.val_injective) hm

Premises used: Subtype.val_injective, LinearMap.annihilator_le_of_injective, Submodule.subtype, le_trans
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
rw :
  (∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0) ↔
    Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
⊢ Subsingleton (LocalizedModule.Away f M) ↔
    Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})

Tactic:
rw [LocalizedModule.subsingleton_iff]

Premises used: LocalizedModule.subsingleton_iff