-- Mathlib/RingTheory/Support.lean
lemma LocalizedModule.subsingleton_iff_support_subset {f : R} :
    Subsingleton (LocalizedModule (.powers f) M) ↔
      Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}

Proof state:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
by_cases h : (Submodule.span R {m}).annihilator = ⊤

Result:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : (Submodule.span R {m}).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(Submodule.span R {m}).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : (Submodule.span R {m}).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
rw [Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot] at h

Result:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : m = 0
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Proof state:
case mp.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : PrimeSpectrum R
hx' : x ∈ Module.support R M
f : R
H : ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0
m : M
hm : (Submodule.span R {m}).annihilator ≤ x.asIdeal
⊢ f ∈ ↑x.asIdeal

Tactic:
obtain ⟨_, ⟨n, rfl⟩, e⟩ := H m

Result:
case mp.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : PrimeSpectrum R
hx' : x ∈ Module.support R M
f : R
H : ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0
m : M
hm : (Submodule.span R {m}).annihilator ≤ x.asIdeal
n : ℕ
e : (fun x => f ^ x) n • m = 0
⊢ f ∈ ↑x.asIdeal

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(Submodule.span R {m}).annihilator = ⊤
p : Ideal R
hp : (Submodule.span R {m}).annihilator ≤ p
hp' : p.IsPrime
⊢ f ∈ p

Tactic:
simpa using H (Module.mem_support_iff_exists_annihilator (p := ⟨p, hp'⟩).mpr ⟨_, hp⟩)

Result:
no goals

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : m = 0
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
exact ⟨1, one_mem _, by simpa using h⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}

Tactic:
constructor

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0) → Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}

case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f} → ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(Submodule.span R {m}).annihilator = ⊤
⊢ f ∈ (Submodule.span R {m}).annihilator.radical

Tactic:
rw [Ideal.radical_eq_sInf, Ideal.mem_sInf]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(Submodule.span R {m}).annihilator = ⊤
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J | (Submodule.span R {m}).annihilator ≤ J ∧ J.IsPrime} → f ∈ I

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : m = 0
⊢ 1 • m = 0

Tactic:
simpa using h

Result:
no goals

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : PrimeSpectrum R
hx' : x ∈ Module.support R M
f : R
H : ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0
⊢ f ∈ ↑x.asIdeal

Tactic:
obtain ⟨m, hm⟩ := Module.mem_support_iff_exists_annihilator.mp hx'

Result:
case mp.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : PrimeSpectrum R
hx' : x ∈ Module.support R M
f : R
H : ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0
m : M
hm : (Submodule.span R {m}).annihilator ≤ x.asIdeal
⊢ f ∈ ↑x.asIdeal

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(Submodule.span R {m}).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
obtain ⟨n, hn⟩ : f ∈ (Submodule.span R {m}).annihilator.radical := by
  rw [Ideal.radical_eq_sInf, Ideal.mem_sInf]
  rintro p ⟨hp, hp'⟩
  simpa using H (Module.mem_support_iff_exists_annihilator (p := ⟨p, hp'⟩).mpr ⟨_, hp⟩)

Result:
case neg.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(Submodule.span R {m}).annihilator = ⊤
n : ℕ
hn : f ^ n ∈ (Submodule.span R {m}).annihilator
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Subsingleton (LocalizedModule (Submonoid.powers f) M) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}

Tactic:
rw [LocalizedModule.subsingleton_iff]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(Submodule.span R {m}).annihilator = ⊤
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J | (Submodule.span R {m}).annihilator ≤ J ∧ J.IsPrime} → f ∈ I

Tactic:
rintro p ⟨hp, hp'⟩

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(Submodule.span R {m}).annihilator = ⊤
p : Ideal R
hp : (Submodule.span R {m}).annihilator ≤ p
hp' : p.IsPrime
⊢ f ∈ p

Proof state:
case mp.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : PrimeSpectrum R
hx' : x ∈ Module.support R M
f : R
H : ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0
m : M
hm : (Submodule.span R {m}).annihilator ≤ x.asIdeal
n : ℕ
e : (fun x => f ^ x) n • m = 0
⊢ f ∈ ↑x.asIdeal

Tactic:
exact Ideal.IsPrime.mem_of_pow_mem inferInstance n
  (hm ((Submodule.mem_annihilator_span_singleton _ _).mpr e))

Result:
no goals

Proof state:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f} → ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
intro H m

Result:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0