-- Mathlib/RingTheory/Support.lean
lemma Module.mem_support_iff_of_span_eq_top {s : Set M} (hs : Submodule.span R s = ⊤) :
    p ∈ Module.support R M ↔ ∃ m ∈ s, (R ∙ m).annihilator ≤ p.asIdeal

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (¬∃ m ∈ s, (Submodule.span R {m}).annihilator ≤ p.asIdeal) → p ∉ support R M

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

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (¬∃ m ∈ s, (Submodule.span R {m}).annihilator ≤ p.asIdeal) →
    ∀ x ∈ s, x ∈ ↑(LinearMap.ker (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M))

Proof state:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
m : M
left✝ : m ∈ s
hm : (Submodule.span R {m}).annihilator ≤ p.asIdeal
⊢ p ∈ support R M

Tactic:
exact mem_support_iff_exists_annihilator.mpr ⟨m, hm⟩

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
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ p ∈ support R M → ∃ m ∈ s, (Submodule.span R {m}).annihilator ≤ p.asIdeal

Tactic:
contrapose

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (¬∃ m ∈ s, (Submodule.span R {m}).annihilator ≤ p.asIdeal) → p ∉ support R M

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (∀ m ∈ s, ∃ x ∉ p.asIdeal, x • m = 0) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0

Tactic:
exact id

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
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (¬∃ m ∈ s, (Submodule.span R {m}).annihilator ≤ p.asIdeal) →
    ∀ x ∈ s, x ∈ ↑(LinearMap.ker (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M))

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

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (¬∃ m ∈ s, ∀ ⦃x : R⦄, x • m = 0 → x ∈ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (∀ m ∈ s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0

Tactic:
simp_rw [and_comm]

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (∀ m ∈ s, ∃ x ∉ p.asIdeal, x • m = 0) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ p ∈ support R M ↔ ∃ m ∈ s, (Submodule.span R {m}).annihilator ≤ p.asIdeal

Tactic:
constructor

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ p ∈ support R M → ∃ m ∈ s, (Submodule.span R {m}).annihilator ≤ p.asIdeal

case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (∃ m ∈ s, (Submodule.span R {m}).annihilator ≤ p.asIdeal) → p ∈ support R M

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (¬∃ m ∈ s, ∀ ⦃x : R⦄, x • m = 0 → x ∈ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0

Tactic:
push_neg

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (∀ m ∈ s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0

Proof state:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (∃ m ∈ s, (Submodule.span R {m}).annihilator ≤ p.asIdeal) → p ∈ support R M

Tactic:
intro ⟨m, _, hm⟩

Result:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
m : M
left✝ : m ∈ s
hm : (Submodule.span R {m}).annihilator ≤ p.asIdeal
⊢ p ∈ support R M