-- 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
inst_3 obtain : Module.Finite R M
obtain₁ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤),
    Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ annihilator R M ≤ p.asIdeal
obtain₂ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤) (H : annihilator R M ≤ p.asIdeal),
    ∃ m ∈ (↑s : Set M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
obtain₃ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (H : ∀ ⦃x : R⦄, Membership.mem (γ := Ideal R) (annihilator R M) x → x ∈ p.asIdeal),
    ∃ m ∈ (↑s : Set M), ∀ ⦃x : R⦄, x • m = 0 → x ∈ p.asIdeal
obtain₄ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (H : ∀ (m : M) (_ : m ∈ (↑s : Set M)), ∃ (x : R), x • m = 0 ∧ x ∉ p.asIdeal),
    ∃ (x : R), Membership.mem (γ := Ideal R) (annihilator R M) x ∧ x ∉ p.asIdeal
obtain₅ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (H : ∀ (m : M) (_ : m ∈ (↑s : Set M)), ∃ (x : R), x • m = 0 ∧ x ∉ p.asIdeal)
    (x : (x : { a : M // a ∈ (↑s : Set M) }) → R) (hx : ∀ (x_1 : { a : M // a ∈ (↑s : Set M) }), x x_1 • (↑x_1 : M) = 0)
    (hx' : ∀ (x_1 : { a : M // a ∈ (↑s : Set M) }), x x_1 ∉ p.asIdeal),
    ∃ (x : R), Membership.mem (γ := Ideal R) (annihilator R M) x ∧ x ∉ p.asIdeal
refine_1 :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (H : ∀ (m : M) (_ : m ∈ (↑s : Set M)), ∃ (x : R), x • m = 0 ∧ x ∉ p.asIdeal)
    (x : (x : { a : M // a ∈ (↑s : Set M) }) → R) (hx : ∀ (x_1 : { a : M // a ∈ (↑s : Set M) }), x x_1 • (↑x_1 : M) = 0)
    (hx' : ∀ (x_1 : { a : M // a ∈ (↑s : Set M) }), x x_1 ∉ p.asIdeal),
    Membership.mem (γ := Ideal R) (annihilator R M) (s.attach.prod x)
refine_2 refine_2₁ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (H : ∀ (m : M) (_ : m ∈ (↑s : Set M)), ∃ (x : R), x • m = 0 ∧ x ∉ p.asIdeal)
    (x : (x : { a : M // a ∈ (↑s : Set M) }) → R) (hx : ∀ (x_1 : { a : M // a ∈ (↑s : Set M) }), x x_1 • (↑x_1 : M) = 0)
    (hx' : ∀ (x_1 : { a : M // a ∈ (↑s : Set M) }), x x_1 ∉ p.asIdeal), s.attach.prod x ∉ p.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ annihilator R M ≤ p.asIdeal

Tactic:
classical
  obtain ⟨s, hs⟩ := ‹Module.Finite R M›
  refine ⟨annihilator_le_of_mem_support, fun H ↦ (mem_support_iff_of_span_eq_top hs).mpr ?_⟩
  simp only [SetLike.le_def, Submodule.mem_annihilator_span_singleton] at H ⊢
  contrapose! H
  choose x hx hx' using Subtype.forall'.mp H
  refine ⟨s.attach.prod x, ?_, ?_⟩
  · rw [← Submodule.annihilator_top, ← hs, Submodule.mem_annihilator_span]
    intro m
    obtain ⟨k, hk⟩ := Finset.dvd_prod_of_mem x (Finset.mem_attach _ m)
    rw [hk, mul_comm, mul_smul, hx, smul_zero]
  · exact p.asIdeal.primeCompl.prod_mem (fun x _ ↦ hx' x)

Premises used: SetLike.le_def, smul_zero, Submodule.mem_annihilator_span, Submodule.annihilator_top, mul_comm, Module.Finite, Submodule.mem_annihilator_span_singleton, SemigroupAction.mul_smul