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
f : R
mp :
  (∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0) →
    Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
mpr :
  Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f}) →
    ∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
⊢ (∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0) ↔
    Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})

Tactic:
constructor
-- 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
x : PrimeSpectrum R
hx' : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M) x
f : R
H : ∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
mp : ∀ (m : M) (hm : Submodule.annihilator (M := M) (R ∙ m) ≤ x.asIdeal), f ∈ (↑x.asIdeal : Set R)
⊢ f ∈ (↑x.asIdeal : Set R)

Tactic:
obtain ⟨m, hm⟩ := Module.mem_support_iff_exists_annihilator.mp hx'

Premises used: Module.mem_support_iff_exists_annihilator, Iff.mp
-- 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
x : PrimeSpectrum R
hx' : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M) x
f : R
H : ∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
m : M
hm : Submodule.annihilator (M := M) (R ∙ m) ≤ x.asIdeal
mp : ∀ (n : ℕ) (e : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ f ^ x) n) m = 0), f ∈ (↑x.asIdeal : Set R)
⊢ f ∈ (↑x.asIdeal : Set R)

Tactic:
obtain ⟨_, ⟨n, rfl⟩, e⟩ := H m

Premises used: rfl
-- 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
x : PrimeSpectrum R
hx' : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M) x
f : R
H : ∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
m : M
hm : Submodule.annihilator (M := M) (R ∙ m) ≤ x.asIdeal
n : ℕ
e : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ f ^ x) n) m = 0
⊢ f ∈ (↑x.asIdeal : Set R)

Tactic:
Ideal.IsPrime.mem_of_pow_mem inferInstance n
      (hm ((Submodule.mem_annihilator_span_singleton _ _).mpr e))

Premises used: Iff.mpr, Ideal.IsPrime.mem_of_pow_mem, inferInstance, 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
x : PrimeSpectrum R
hx' : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M) x
f : R
H : ∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
m : M
hm : Submodule.annihilator (M := M) (R ∙ m) ≤ x.asIdeal
n : ℕ
e : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ f ^ x) n) m = 0
⊢ f ∈ (↑x.asIdeal : Set R)

Tactic:
exact Ideal.IsPrime.mem_of_pow_mem inferInstance n
      (hm ((Submodule.mem_annihilator_span_singleton _ _).mpr e))

Premises used: Iff.mpr, Ideal.IsPrime.mem_of_pow_mem, inferInstance, 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
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
pos :
  ∀ (h : Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤),
    ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
neg :
  ∀ (h : ¬Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤),
    ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
⊢ ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0

Tactic:
by_cases h : (Submodule.span R {m}).annihilator = ⊤

Premises used: Submodule.span, Singleton.singleton, Submodule.annihilator
-- 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
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
h : Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤
⊢ m = 0

Tactic:
rw [Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot] at h

Premises used: Submodule.span_singleton_eq_bot, Submodule.annihilator_eq_top_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
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
h : m = 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = 0

Tactic:
simpa using 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
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
h : m = 0
⊢ ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0

Tactic:
exact ⟨1, one_mem _, by simpa using 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
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
h : ¬Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤
rw :
  ∀ ⦃I : Ideal R⦄,
    Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Submodule.annihilator (M := M) (R ∙ m) ≤ J ∧ J.IsPrime} I → f ∈ I
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (Submodule.annihilator (M := M) (R ∙ m))) f

Tactic:
rw [Ideal.radical_eq_sInf, Ideal.mem_sInf]

Premises used: Ideal.mem_sInf, Ideal.radical_eq_sInf
-- 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
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
h : ¬Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤
p : Ideal R
hp : Submodule.annihilator (M := M) (R ∙ m) ≤ p
hp' : p.IsPrime
⊢ f ∈ p

Tactic:
simpa using H (Module.mem_support_iff_exists_annihilator (p := ⟨p, hp'⟩).mpr ⟨_, hp⟩)

Premises used: Iff.mpr, Module.mem_support_iff_exists_annihilator, 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
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
h : ¬Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤
neg :
  ∀ (n : ℕ) (hn : Membership.mem (γ := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) (f ^ n)),
    ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0
⊢ ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0

Tactic:
obtain ⟨n, hn⟩ : f ∈ (Submodule.span R {m}).annihilator.radical := by
      rw [Ideal.radical_eq_sInf, Ideal.mem_sInf]
      rintro p ⟨hp, hp'⟩
      simpa using H (Module.mem_support_iff_exists_annihilator (p := ⟨p, hp'⟩).mpr ⟨_, hp⟩)

Premises used: Submodule.span, Singleton.singleton, Ideal.radical, Submodule.annihilator
-- 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
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
h : ¬Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤
n : ℕ
hn : Membership.mem (γ := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) (f ^ n)
⊢ ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0

Tactic:
⟨_, ⟨n, rfl⟩, (Submodule.mem_annihilator_span_singleton _ _).mp hn⟩

Premises used: And.intro, Exists.intro, Iff.mp, Submodule.mem_annihilator_span_singleton, rfl
-- 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
f : R
H : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
m : M
h : ¬Eq (α := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) ⊤
n : ℕ
hn : Membership.mem (γ := Ideal R) (Submodule.annihilator (M := M) (R ∙ m)) (f ^ n)
⊢ ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) r ∧ r • m = 0

Tactic:
exact ⟨_, ⟨n, rfl⟩, (Submodule.mem_annihilator_span_singleton _ _).mp hn⟩
-- 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
rw : (∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers 1) r ∧ r • m = 0) ↔ ∀ (y : M), y = 0
⊢ Eq (α := Set (PrimeSpectrum R)) (support R M) ∅ ↔ Subsingleton M

Tactic:
rw [← Set.subset_empty_iff, ← PrimeSpectrum.zeroLocus_singleton_one,
    ← LocalizedModule.subsingleton_iff_support_subset, LocalizedModule.subsingleton_iff,
    subsingleton_iff_forall_eq 0]

Premises used: subsingleton_iff_forall_eq, LocalizedModule.subsingleton_iff, LocalizedModule.subsingleton_iff_support_subset, PrimeSpectrum.zeroLocus_singleton_one, Set.subset_empty_iff, OfNat.ofNat
-- 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
⊢ (∀ (m : M), ∃ (r : R), Membership.mem (γ := Submonoid R) (Submonoid.powers 1) r ∧ r • m = 0) ↔ ∀ (y : M), y = 0

Tactic:
simp only [Submonoid.powers_one, Submonoid.mem_bot, exists_eq_left, one_smul]

Premises used: Submonoid.powers_one, Submonoid.mem_bot, exists_eq_left, one_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
rw : Ne (α := Set (PrimeSpectrum R)) (support R M) ∅ ↔ Nontrivial M
rw₁ : ¬Eq (α := Set (PrimeSpectrum R)) (support R M) ∅ ↔ Nontrivial M
rw₂ : ¬Subsingleton M ↔ Nontrivial M
rw₃ rw₄ : ¬Subsingleton M ↔ ¬Subsingleton M
⊢ Set.Nonempty (α := PrimeSpectrum R) (support R M) ↔ Nontrivial M

Tactic:
rw [Set.nonempty_iff_ne_empty, ne_eq,
    Module.support_eq_empty_iff, ← not_subsingleton_iff_nontrivial]

Premises used: ne_eq, Module.support_eq_empty_iff, Set.nonempty_iff_ne_empty, not_subsingleton_iff_nontrivial
-- 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 : Nontrivial M
⊢ Set.Nonempty (α := PrimeSpectrum R) (support R M)

Tactic:
Module.nonempty_support_iff.mpr ‹_›

Premises used: Iff.mpr, Module.nonempty_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 : Subsingleton M
⊢ Eq (α := Set (PrimeSpectrum R)) (support R M) ∅

Tactic:
Module.support_eq_empty_iff.mpr ‹_›

Premises used: Iff.mpr, Module.support_eq_empty_iff
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
h :
  ∀ (p : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R)) (support R A) p ↔
      Membership.mem (γ := Set (PrimeSpectrum R))
        (PrimeSpectrum.zeroLocus (↑(RingHom.ker (F := R →+* A) (algebraMap R A)) : Set R)) p
⊢ Eq (α := Set (PrimeSpectrum R)) (support R A)
    (PrimeSpectrum.zeroLocus (↑(RingHom.ker (F := R →+* A) (algebraMap R A)) : Set R))

Tactic:
ext p
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
p : PrimeSpectrum R
h : (∃ (m : A), ∀ r ∉ p.asIdeal, ¬r • m = 0) ↔ RingHom.ker (F := R →+* A) (algebraMap R A) ≤ p.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R A) p ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (PrimeSpectrum.zeroLocus (↑(RingHom.ker (F := R →+* A) (algebraMap R A)) : Set R)) p

Tactic:
simp only [mem_support_iff', ne_eq, PrimeSpectrum.mem_zeroLocus, SetLike.coe_subset_coe]

Premises used: PrimeSpectrum.mem_zeroLocus, Module.mem_support_iff', ne_eq, SetLike.coe_subset_coe
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
p : PrimeSpectrum R
⊢ (∃ (m : A), ∀ r ∉ p.asIdeal, ¬r • m = 0) ↔ RingHom.ker (F := R →+* A) (algebraMap R A) ≤ p.asIdeal

Tactic:
⟨fun ⟨m, hm⟩ x hx ↦ not_not.mp fun hx' ↦ ?_, fun H ↦ ⟨1, fun r hr e ↦ ?_⟩⟩

Premises used: Classical.not_not, Membership.mem, _private.0.Module.support_of_algebra.match_3, Iff.intro, Exists.intro, Iff.mp, OfNat.ofNat, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
p : PrimeSpectrum R
h :
  (∃ (m : A), ∀ r ∉ p.asIdeal, ¬r • m = 0) →
    ∀ (x : R) (hx : Membership.mem (γ := Submodule R R) (RingHom.ker (F := R →+* A) (algebraMap R A)) x) (m : A)
      (hm : ∀ r ∉ p.asIdeal, ¬r • m = 0) (hx' : x ∉ p.asIdeal), False
h₁ :
  ∀ (H : RingHom.ker (F := R →+* A) (algebraMap R A) ≤ p.asIdeal) (r : R) (hr : r ∉ p.asIdeal)
    (e : HSMul.hSMul (β := A) r 1 = 0), False
⊢ (∃ (m : A), ∀ r ∉ p.asIdeal, ¬r • m = 0) ↔ RingHom.ker (F := R →+* A) (algebraMap R A) ≤ p.asIdeal

Tactic:
refine ⟨fun ⟨m, hm⟩ x hx ↦ not_not.mp fun hx' ↦ ?_, fun H ↦ ⟨1, fun r hr e ↦ ?_⟩⟩
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
p : PrimeSpectrum R
h : ∃ (m : A), ∀ r ∉ p.asIdeal, ¬r • m = 0
x : R
hx : Membership.mem (γ := Submodule R R) (RingHom.ker (F := R →+* A) (algebraMap R A)) x
m : A
hm : ∀ r ∉ p.asIdeal, ¬r • m = 0
hx' : x ∉ p.asIdeal
⊢ False

Tactic:
simpa [Algebra.smul_def, (show _ = _ from hx)] using hm _ hx'

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
p : PrimeSpectrum R
H : RingHom.ker (F := R →+* A) (algebraMap R A) ≤ p.asIdeal
r : R
hr : r ∉ p.asIdeal
e : HSMul.hSMul (β := A) r 1 = 0
⊢ False

Tactic:
hr (H ((Algebra.algebraMap_eq_smul_one _).trans e))

Premises used: Algebra.algebraMap_eq_smul_one, Eq.trans
-- Module: Mathlib.RingTheory.Support
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
p : PrimeSpectrum R
H : RingHom.ker (F := R →+* A) (algebraMap R A) ≤ p.asIdeal
r : R
hr : r ∉ p.asIdeal
e : HSMul.hSMul (β := A) r 1 = 0
⊢ False

Tactic:
exact hr (H ((Algebra.algebraMap_eq_smul_one _).trans e))

Premises used: Algebra.algebraMap_eq_smul_one, Eq.trans
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Nontrivial M
simp : ∀ (x : PrimeSpectrum R), ∃ (m : M), ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0
⊢ Eq (α := Set (PrimeSpectrum R)) (support R M) Set.univ

Tactic:
simp only [Set.eq_univ_iff_forall, mem_support_iff', ne_eq, smul_eq_zero, not_or]

Premises used: Set.eq_univ_iff_forall, Module.mem_support_iff', ne_eq, not_or, smul_eq_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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Nontrivial M
obtain : ∀ (x : M) (hx : x ≠ 0) (x : PrimeSpectrum R), ∃ (m : M), ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0
⊢ ∀ (x : PrimeSpectrum R), ∃ (m : M), ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : M)

Premises used: exists_ne, OfNat.ofNat
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Nontrivial M
x : M
hx : x ≠ 0
⊢ ∀ (x : PrimeSpectrum R), ∃ (m : M), ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0

Tactic:
fun p ↦ ⟨x, fun r hr ↦ ⟨fun e ↦ hr (e ▸ p.asIdeal.zero_mem), hx⟩⟩

Premises used: Eq.rec, Ideal.zero_mem, And.intro, Exists.intro, Eq.symm, 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 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Nontrivial M
x : M
hx : x ≠ 0
⊢ ∀ (x : PrimeSpectrum R), ∃ (m : M), ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0

Tactic:
exact fun p ↦ ⟨x, fun r hr ↦ ⟨fun e ↦ hr (e ▸ p.asIdeal.zero_mem), hx⟩⟩
-- 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
f : M →ₗ[R] N
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
simp_rw : ∀ (x : PrimeSpectrum R), (∃ (m : M), ∀ r ∉ x.asIdeal, r • m ≠ 0) → ∃ (m : N), ∀ r ∉ x.asIdeal, r • m ≠ 0
⊢ Subset (α := Set (PrimeSpectrum R)) (support R M) (support R N)

Tactic:
simp_rw [Set.subset_def, mem_support_iff']

Premises used: Set.subset_def, Module.mem_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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : PrimeSpectrum R
m : M
hm : ∀ r ∉ x.asIdeal, r • m ≠ 0
r : R
hr : r ∉ x.asIdeal
⊢ HSMul.hSMul (β := N) r ((f : (a : M) → N) m : N) ≠ 0

Tactic:
simpa using hf.ne (hm r hr)

Premises used: Function.Injective.ne
-- 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
f : M →ₗ[R] N
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : PrimeSpectrum R
m : M
hm : ∀ r ∉ x.asIdeal, r • m ≠ 0
⊢ ∃ (m : N), ∀ r ∉ x.asIdeal, r • m ≠ 0

Tactic:
exact ⟨f m, fun r hr ↦ by simpa using hf.ne (hm r hr)⟩
-- 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
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
simp_rw : ∀ (x : PrimeSpectrum R), (∃ (m : N), ∀ r ∉ x.asIdeal, r • m ≠ 0) → ∃ (m : M), ∀ r ∉ x.asIdeal, r • m ≠ 0
⊢ Subset (α := Set (PrimeSpectrum R)) (support R N) (support R M)

Tactic:
simp_rw [Set.subset_def, mem_support_iff']

Premises used: Set.subset_def, Module.mem_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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : PrimeSpectrum R
m : N
hm : ∀ r ∉ x.asIdeal, r • m ≠ 0
obtain :
  ∀ (m : M) (hm : ∀ r ∉ x.asIdeal, HSMul.hSMul (β := N) r ((f : (a : M) → N) m : N) ≠ 0),
    ∃ (m : M), ∀ r ∉ x.asIdeal, r • m ≠ 0
⊢ ∃ (m : M), ∀ r ∉ x.asIdeal, r • m ≠ 0

Tactic:
obtain ⟨m, rfl⟩ := hf m

Premises used: rfl
-- 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
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : PrimeSpectrum R
m : M
hm : ∀ r ∉ x.asIdeal, HSMul.hSMul (β := N) r ((f : (a : M) → N) m : N) ≠ 0
r : R
hr : r ∉ x.asIdeal
e : r • m = 0
⊢ HSMul.hSMul (β := N) r ((f : (a : M) → N) m : N) = 0

Tactic:
simpa using congr(f $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
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : PrimeSpectrum R
m : M
hm : ∀ r ∉ x.asIdeal, HSMul.hSMul (β := N) r ((f : (a : M) → N) m : N) ≠ 0
⊢ ∃ (m : M), ∀ r ∉ x.asIdeal, r • m ≠ 0

Tactic:
exact ⟨m, fun r hr e ↦ hm r hr (by simpa using congr(f $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)
⊢ Eq (α := Set (PrimeSpectrum R)) (support R N) (support R M ∪ support R P)

Tactic:
subset_antisymm ?_ (Set.union_subset (Module.support_subset_of_injective f hf)
    (Module.support_subset_of_surjective g hg))

Premises used: subset_antisymm, Set.union_subset, Module.support_subset_of_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
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)
refine : Subset (α := Set (PrimeSpectrum R)) (support R N) (support R M ∪ support R P)
⊢ Eq (α := Set (PrimeSpectrum R)) (support R N) (support R M ∪ support R P)

Tactic:
refine subset_antisymm ?_ (Set.union_subset (Module.support_subset_of_injective f hf)
    (Module.support_subset_of_surjective g hg))

Premises used: subset_antisymm, Set.union_subset, Module.support_subset_of_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
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
contrapose : x ∉ support R M ∪ support R P → x ∉ support R N
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R N) x →
    Membership.mem (γ := Set (PrimeSpectrum R)) (support R M ∪ support R P) x

Tactic:
contrapose
-- 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
simp :
  (∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0) →
    (∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0) → ∀ (m : N), ∃ r ∉ x.asIdeal, r • m = 0
⊢ x ∉ support R M ∪ support R P → x ∉ support R N

Tactic:
simp only [Set.mem_union, not_or, and_imp, notMem_support_iff']

Premises used: Set.mem_union, and_imp, not_or, Module.notMem_support_iff'