-- Mathlib/RingTheory/Support.lean
/-- If `M` is a finite module such that `Mₚ = 0` for some `p`,
then `M[1/f] = 0` for some `p ∈ D(f)`. -/
lemma LocalizedModule.exists_subsingleton_away [Module.Finite R M] (p : Ideal R) [p.IsPrime]
    [Subsingleton (LocalizedModule p.primeCompl M)] :
    ∃ f ∉ p, Subsingleton (LocalizedModule (.powers f) M)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
⊢ { asIdeal := p, isPrime := ⋯ } ∈ (Module.support R M)ᶜ

Tactic:
simpa [Module.not_mem_support_iff]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
f : R
hf : f ∈ ↑(Module.annihilator R M)
hf' : { asIdeal := p, isPrime := ⋯ } ∈ (PrimeSpectrum.zeroLocus {f})ᶜ
⊢ f ∉ p

Tactic:
simpa using hf'

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)

Tactic:
have : ⟨p, inferInstance⟩ ∈ (Module.support R M)ᶜ := by
  simpa [Module.not_mem_support_iff]

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
this : { asIdeal := p, isPrime := ⋯ } ∈ (Module.support R M)ᶜ
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
f : R
hf : f ∈ ↑(Module.annihilator R M)
hf' : { asIdeal := p, isPrime := ⋯ } ∈ (PrimeSpectrum.zeroLocus {f})ᶜ
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)

Tactic:
exact ⟨f, by simpa using hf', subsingleton_iff.mpr
  fun m ↦ ⟨f, Submonoid.mem_powers f, Module.mem_annihilator.mp hf _⟩⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
this : ∃ i, ∃ (_ : i ∈ ↑(Module.annihilator R M)), { asIdeal := p, isPrime := ⋯ } ∈ (PrimeSpectrum.zeroLocus {i})ᶜ
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)

Tactic:
obtain ⟨f, hf, hf'⟩ := this

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
f : R
hf : f ∈ ↑(Module.annihilator R M)
hf' : { asIdeal := p, isPrime := ⋯ } ∈ (PrimeSpectrum.zeroLocus {f})ᶜ
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
this : { asIdeal := p, isPrime := ⋯ } ∈ (Module.support R M)ᶜ
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)

Tactic:
rw [Module.support_eq_zeroLocus, ← Set.biUnion_of_singleton (Module.annihilator R M : Set R),
  PrimeSpectrum.zeroLocus_iUnion₂, Set.compl_iInter₂, Set.mem_iUnion₂] at this

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
this : ∃ i, ∃ (_ : i ∈ ↑(Module.annihilator R M)), { asIdeal := p, isPrime := ⋯ } ∈ (PrimeSpectrum.zeroLocus {i})ᶜ
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)