awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
obtain :
  ∀ (r : R) (hr : r ∉ x.asIdeal) (e₁ : HSMul.hSMul (β := P) r ((g : (a : N) → P) m : P) = 0), ∃ r ∉ x.asIdeal, r • m = 0
⊢ ∃ r ∉ x.asIdeal, r • m = 0

Tactic:
obtain ⟨r, hr, e₁⟩ := H₂ (g m)

Premises used: DFunLike.coe
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
e₁ : HSMul.hSMul (β := P) r ((g : (a : N) → P) m : P) = 0
⊢ Membership.mem (γ := Set N) (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → N)) (r • m)

Tactic:
rw [← map_smul, h] at e₁

Premises used: map_smul
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
e₁ : Membership.mem (γ := Set N) (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → N)) (r • m)
obtain : ∀ (m' : M) (hm' : (f : (a : M) → N) m' = r • m), ∃ r ∉ x.asIdeal, r • m = 0
⊢ ∃ r ∉ x.asIdeal, r • m = 0

Tactic:
obtain ⟨m', hm'⟩ := e₁
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : (f : (a : M) → N) m' = r • m
obtain : ∀ (s : R) (hs : s ∉ x.asIdeal) (e₁ : s • m' = 0), ∃ r ∉ x.asIdeal, r • m = 0
⊢ ∃ r ∉ x.asIdeal, r • m = 0

Tactic:
obtain ⟨s, hs, e₁⟩ := H₁ m'
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : (f : (a : M) → N) m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
rw : s • r • m = 0
rw₁ : HSMul.hSMul (β := N) s ((f : (a : M) → N) m' : N) = 0
rw₂ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (s • m') : N) (0 : N)
rw₃ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
rw₄ rw₅ : Eq.{u_3 + 1} (α := N) 0 0
⊢ (s * r) • m = 0

Tactic:
rw [mul_smul, ← hm', ← map_smul, e₁, map_zero]

Premises used: map_zero, SemigroupAction.mul_smul, map_smul
-- 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
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : (f : (a : M) → N) m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
⊢ ∃ r ∉ x.asIdeal, r • m = 0

Tactic:
exact ⟨_, x.asIdeal.primeCompl.mul_mem hs hr, by rw [mul_smul, ← hm', ← map_smul, e₁, map_zero]⟩
-- 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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
⊢ Eq (α := Set (PrimeSpectrum R)) (Module.support R M) (Module.support R N)

Tactic:
(Module.support_subset_of_injective e.toLinearMap e.injective).antisymm
    (Module.support_subset_of_surjective e.toLinearMap e.surjective)

Premises used: LinearEquiv.surjective, LinearEquiv.toLinearMap, HasSubset.Subset.antisymm, Module.support_subset_of_injective, LinearEquiv.injective, Module.support_subset_of_surjective
-- 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 : 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

Tactic:
obtain ⟨s, hs⟩ := ‹Module.Finite R M›

Premises used: Module.Finite
-- 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 : 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

Tactic:
⟨annihilator_le_of_mem_support, fun H ↦ (mem_support_iff_of_span_eq_top hs).mpr ?_⟩

Premises used: Iff.mpr, Iff.intro, Module.mem_support_iff_of_span_eq_top, Module.annihilator_le_of_mem_support
-- 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 : Module.Finite R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
refine : ∀ (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

Tactic:
refine ⟨annihilator_le_of_mem_support, fun H ↦ (mem_support_iff_of_span_eq_top hs).mpr ?_⟩
-- 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 : Module.Finite R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
H : annihilator R M ≤ p.asIdeal
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
⊢ ∃ m ∈ (↑s : Set M), Submodule.annihilator (M := M) (R ∙ m) ≤ p.asIdeal

Tactic:
simp only [SetLike.le_def, Submodule.mem_annihilator_span_singleton] at H ⊢

Premises used: SetLike.le_def, Submodule.mem_annihilator_span_singleton
-- 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 : 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
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
⊢ ∃ m ∈ (↑s : Set M), ∀ ⦃x : R⦄, x • m = 0 → x ∈ p.asIdeal

Tactic:
contrapose! H
-- 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 : 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
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
⊢ ∃ (x : R), Membership.mem (γ := Ideal R) (annihilator R M) x ∧ x ∉ p.asIdeal

Tactic:
choose x hx hx' using Subtype.forall'.mp H

Premises used: Iff.mp, Subtype.forall'
-- 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 : 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

Tactic:
⟨s.attach.prod x, ?_, ?_⟩

Premises used: Finset.prod, And.intro, Finset.attach, Exists.intro
-- 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 : 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)
refine_2 : s.attach.prod x ∉ p.asIdeal
⊢ ∃ (x : R), Membership.mem (γ := Ideal R) (annihilator R M) x ∧ x ∉ p.asIdeal

Tactic:
refine ⟨s.attach.prod x, ?_, ?_⟩
-- 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 : 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 : ∀ (n : (↑(↑s : Set M) : Type u_2)), s.attach.prod x • (↑n : M) = 0
⊢ Membership.mem (γ := Ideal R) (annihilator R M) (s.attach.prod x)

Tactic:
rw [← Submodule.annihilator_top, ← hs, Submodule.mem_annihilator_span]

Premises used: Submodule.mem_annihilator_span, Submodule.annihilator_top
-- 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 : 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)
refine_1 : ∀ (k : R) (hk : ∏ i ∈ s.attach, x i = x m * k), s.attach.prod x • (↑m : M) = 0
⊢ s.attach.prod x • (↑m : M) = 0

Tactic:
obtain ⟨k, hk⟩ := Finset.dvd_prod_of_mem x (Finset.mem_attach _ m)

Premises used: Finset.dvd_prod_of_mem, Finset.mem_attach
-- 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 : 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
refine_1₄ refine_1₅ : Eq.{u_2 + 1} (α := M) 0 0
⊢ s.attach.prod x • (↑m : M) = 0

Tactic:
rw [hk, mul_comm, mul_smul, hx, smul_zero]

Premises used: smul_zero, mul_comm, SemigroupAction.mul_smul
-- 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 : 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
⊢ s.attach.prod x ∉ p.asIdeal

Tactic:
p.asIdeal.primeCompl.prod_mem (fun x _ ↦ hx' x)

Premises used: Submonoid.prod_mem, Set.Mem, setOf, Ideal.primeCompl, PrimeSpectrum.asIdeal, Not
-- 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 : 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
⊢ s.attach.prod x ∉ p.asIdeal

Tactic:
exact p.asIdeal.primeCompl.prod_mem (fun x _ ↦ hx' x)

Premises used: Submonoid.prod_mem, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- 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
inst_3 : Module.Finite R M
⊢ Eq (α := Set (PrimeSpectrum R)) (support R M) (zeroLocus (↑(annihilator R M) : Set R))

Tactic:
Set.ext fun _ ↦ mem_support_iff_of_finite

Premises used: Set.ext, Module.mem_support_iff_of_finite
-- 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
inst_3 : Module.Finite R M
p : Ideal R
inst_4 : p.IsPrime
inst_5 : Subsingleton (LocalizedModule p.primeCompl M)
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M)ᶜ { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }

Tactic:
simpa [Module.notMem_support_iff]

Premises used: Module.notMem_support_iff
-- 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
inst_3 : Module.Finite R M
p : Ideal R
inst_4 : p.IsPrime
inst_5 : Subsingleton (LocalizedModule p.primeCompl M)
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M)ᶜ { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }

Tactic:
have : ⟨p, inferInstance⟩ ∈ (Module.support R M)ᶜ := by
    simpa [Module.notMem_support_iff]
-- 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
inst_3 : Module.Finite R M
p : Ideal R
inst_4 : p.IsPrime
inst_5 : Subsingleton (LocalizedModule p.primeCompl M)
this :
  Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M)ᶜ { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }
⊢ ∃ (i : R) (_ : i ∈ (↑(Module.annihilator R M) : Set R)),
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {i})ᶜ { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }

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

Premises used: Set.compl_iInter₂, Module.annihilator, Set.biUnion_of_singleton, Set.mem_iUnion₂, SetLike.coe, PrimeSpectrum.zeroLocus_iUnion₂, Module.support_eq_zeroLocus
-- 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
inst_3 : Module.Finite R M
p : Ideal R
inst_4 : p.IsPrime
inst_5 : Subsingleton (LocalizedModule p.primeCompl M)
this :
  ∃ (i : R) (_ : i ∈ (↑(Module.annihilator R M) : Set R)),
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {i})ᶜ { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }
obtain :
  ∀ (f : R) (hf : f ∈ (↑(Module.annihilator R M) : Set R))
    (hf' :
      Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f})ᶜ { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }),
    ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)

Tactic:
obtain ⟨f, hf, hf'⟩ := this
-- 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
inst_3 : Module.Finite R M
p : Ideal R
inst_4 : p.IsPrime
inst_5 : Subsingleton (LocalizedModule p.primeCompl M)
f : R
hf : f ∈ (↑(Module.annihilator R M) : Set R)
hf' : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f})ᶜ { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }
⊢ f ∉ p

Tactic:
simpa using hf'
-- 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
inst_3 : Module.Finite R M
p : Ideal R
inst_4 : p.IsPrime
inst_5 : Subsingleton (LocalizedModule p.primeCompl M)
f : R
hf : f ∈ (↑(Module.annihilator R M) : Set R)
hf' : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f})ᶜ { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)

Tactic:
exact ⟨f, by simpa using hf', subsingleton_iff.mpr
    fun m ↦ ⟨f, Submonoid.mem_powers f, Module.mem_annihilator.mp hf _⟩⟩
-- 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
inst_3 : Module.Finite R M
M' : Type u_5
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
l : M →ₗ[R] M'
p : Ideal R
inst_6 : p.IsPrime
inst_7 : IsLocalizedModule p.primeCompl l
inst_8 : Subsingleton M'
e : LocalizedModule p.primeCompl M ≃ₗ[R] M' := iso p.primeCompl l
⊢ Subsingleton (LocalizedModule p.primeCompl M)

Tactic:
have : Subsingleton (LocalizedModule p.primeCompl M) := e.subsingleton
-- 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
inst_3 : Module.Finite R M
M' : Type u_5
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
l : M →ₗ[R] M'
p : Ideal R
inst_6 : p.IsPrime
inst_7 : IsLocalizedModule p.primeCompl l
inst_8 : Subsingleton M'
e : LocalizedModule p.primeCompl M ≃ₗ[R] M' := iso p.primeCompl l
this : Subsingleton (LocalizedModule p.primeCompl M)
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)

Tactic:
LocalizedModule.exists_subsingleton_away p

Premises used: LocalizedModule.exists_subsingleton_away
-- 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
inst_3 : Module.Finite R M
M' : Type u_5
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
l : M →ₗ[R] M'
p : Ideal R
inst_6 : p.IsPrime
inst_7 : IsLocalizedModule p.primeCompl l
inst_8 : Subsingleton M'
e : LocalizedModule p.primeCompl M ≃ₗ[R] M' := iso p.primeCompl l
this : Subsingleton (LocalizedModule p.primeCompl M)
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)

Tactic:
exact LocalizedModule.exists_subsingleton_away p

Premises used: LocalizedModule.exists_subsingleton_away
-- 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
inst_3 : Module.Finite R M
I : Ideal R
a :
  Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
    (support R M ∩ zeroLocus (↑I : Set R))
a₁ :
  Subset (α := Set (PrimeSpectrum R)) (support R M ∩ zeroLocus (↑I : Set R))
    (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
⊢ Eq (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
    (support R M ∩ zeroLocus (↑I : Set R))

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- 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
inst_3 : Module.Finite R M
I : Ideal R
⊢ Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
    (support R M ∩ zeroLocus (↑I : Set R))

Tactic:
Set.subset_inter ?_ ?_

Premises used: Set.subset_inter
-- 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
inst_3 : Module.Finite R M
I : Ideal R
a : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)) (support R M)
a₁ :
  Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
    (zeroLocus (↑I : Set R))
⊢ Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
    (support R M ∩ zeroLocus (↑I : Set R))

Tactic:
refine Set.subset_inter ?_ ?_

Premises used: Set.subset_inter
-- 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
inst_3 : Module.Finite R M
I : Ideal R
⊢ Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)) (support R M)

Tactic:
Module.support_subset_of_surjective _ (Submodule.mkQ_surjective _)

Premises used: Submodule.mkQ_surjective, Module.support_subset_of_surjective
-- 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
inst_3 : Module.Finite R M
I : Ideal R
⊢ Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)) (support R M)

Tactic:
exact Module.support_subset_of_surjective _ (Submodule.mkQ_surjective _)

Premises used: Submodule.mkQ_surjective, Module.support_subset_of_surjective
-- 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
inst_3 : Module.Finite R M
I : Ideal R
a :
  Subset (α := Set (PrimeSpectrum R))
    (zeroLocus (↑(annihilator.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)) : Set R))
    (zeroLocus (↑I : Set R))
⊢ Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
    (zeroLocus (↑I : Set R))

Tactic:
rw [support_eq_zeroLocus]

Premises used: Module.support_eq_zeroLocus