awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ annihilator R M ≤ p.asIdeal
have 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
Tactic: obtain ⟨s, hs⟩ := ‹Module.Finite R M›
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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
have refine : ∀ (H : annihilator R M ≤ p.asIdeal), ∃ m ∈ (↑s : Set M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal
Tactic: refine ⟨annihilator_le_of_mem_support, fun H ↦ (mem_support_iff_of_span_eq_top hs).mpr ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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
have simp : ∀ (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
Tactic: simp only [SetLike.le_def, Submodule.mem_annihilator_span_singleton] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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
have contrapose! : ∀ (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
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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
have choose : ∀ (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
Tactic: choose x hx hx' using Subtype.forall'.mp H
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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
have refine_1 : Membership.mem (γ := Ideal R) (annihilator R M) (s.attach.prod x)
Tactic: refine ⟨s.attach.prod x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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
refine_1 : Membership.mem (γ := Ideal R) (annihilator R M) (s.attach.prod x)
⊢ ∃ (x : R), Membership.mem (γ := Ideal R) (annihilator R M) x ∧ x ∉ p.asIdeal
have refine_2 : s.attach.prod x ∉ p.asIdeal
Tactic: refine ⟨s.attach.prod x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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)
have refine_1 : ∀ (n : (↑(↑s : Set M) : Type u_2)), s.attach.prod x • (↑n : M) = 0
Tactic: rw [← Submodule.annihilator_top, ← hs, Submodule.mem_annihilator_span]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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
m : (↑(↑s : Set M) : Type u_2)
⊢ s.attach.prod x • (↑m : M) = 0
have refine_1 : ∀ (k : R) (hk : ∏ i ∈ s.attach, x i = x m * k), s.attach.prod x • (↑m : M) = 0
Tactic: obtain ⟨k, hk⟩ := Finset.dvd_prod_of_mem x (Finset.mem_attach _ m)
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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
m : (↑(↑s : Set M) : Type u_2)
k : R
hk : ∏ i ∈ s.attach, x i = x m * k
⊢ s.attach.prod x • (↑m : M) = 0
have refine_1 : (x m * k) • (↑m : M) = 0
Tactic: rw [hk, mul_comm, mul_smul, hx, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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
m : (↑(↑s : Set M) : Type u_2)
k : R
hk : ∏ i ∈ s.attach, x i = x m * k
refine_1 : (x m * k) • (↑m : M) = 0
⊢ s.attach.prod x • (↑m : M) = 0
have refine_1₁ : (k * x m) • (↑m : M) = 0
Tactic: rw [hk, mul_comm, mul_smul, hx, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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
m : (↑(↑s : Set M) : Type u_2)
k : R
hk : ∏ i ∈ s.attach, x i = x m * k
refine_1 : (x m * k) • (↑m : M) = 0
refine_1₁ : (k * x m) • (↑m : M) = 0
⊢ s.attach.prod x • (↑m : M) = 0
have refine_1₂ : k • x m • (↑m : M) = 0
Tactic: rw [hk, mul_comm, mul_smul, hx, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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
m : (↑(↑s : Set M) : Type u_2)
k : R
hk : ∏ i ∈ s.attach, x i = x m * k
refine_1 : (x m * k) • (↑m : M) = 0
refine_1₁ : (k * x m) • (↑m : M) = 0
refine_1₂ : k • x m • (↑m : M) = 0
⊢ s.attach.prod x • (↑m : M) = 0
have refine_1₃ : HSMul.hSMul (β := M) k 0 = 0
Tactic: rw [hk, mul_comm, mul_smul, hx, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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 : Module.Finite R M
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
m : (↑(↑s : Set M) : Type u_2)
k : R
hk : ∏ i ∈ s.attach, x i = x m * k
refine_1 : (x m * k) • (↑m : M) = 0
refine_1₁ : (k * x m) • (↑m : M) = 0
refine_1₂ : k • x m • (↑m : M) = 0
refine_1₃ : HSMul.hSMul (β := M) k 0 = 0
⊢ s.attach.prod x • (↑m : M) = 0
have refine_1₄ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [hk, mul_comm, mul_smul, hx, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ annihilator R M ≤ p.asIdeal
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ annihilator R M ≤ p.asIdeal
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ annihilator R M ≤ p.asIdeal
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ annihilator R M ≤ p.asIdeal
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ annihilator R M ≤ p.asIdeal
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ annihilator R M ≤ p.asIdeal
have 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)
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)
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
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)
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ annihilator R M ≤ p.asIdeal
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.Support (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
p : Ideal R
inst_4 : p.IsPrime
inst_5 : Subsingleton (LocalizedModule p.primeCompl M)
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)
have this : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M)ᶜ { asIdeal := p, isPrime := sorry : PrimeSpectrum R }
Tactic: have : ⟨p, inferInstance⟩ ∈ (Module.support R M)ᶜ := by
    simpa [Module.notMem_support_iff]