awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
a : R
ha : a ∈ (↑T : Set R)
refine_1 :
  ∀ (u : ↥S) (hu : ∏ a : ↥T, g a = g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) * u),
    ∃ (n : ℕ), a ^ n • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m = 0
⊢ ∃ (n : ℕ), a ^ n • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m = 0

Tactic:
obtain ⟨u, hu⟩ : g ⟨a, ha⟩ ∣ (∏ a, g a) := by
      apply Finset.dvd_prod_of_mem g (Finset.mem_univ ⟨a, ha⟩)

Premises used: Finset.univ, Finset.prod, Subtype.mk
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
a : R
ha : a ∈ (↑T : Set R)
u : ↥S
hu : ∏ a : ↥T, g a = g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) * u
h :
  a ^ e (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m = 0
⊢ ∃ (n : ℕ), a ^ n • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m = 0

Tactic:
use e ⟨a, ha⟩

Premises used: Subtype.mk
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
a : R
ha : a ∈ (↑T : Set R)
u : ↥S
hu : ∏ a : ↥T, g a = g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) * u
h :
  (↑u : R) •
      (↑(g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha)) : R) • a ^ e (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) • m =
    0
⊢ a ^ e (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) • HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m = 0

Tactic:
rw [hu, Submonoid.coe_mul, smul_smul, ← mul_assoc, mul_comm, ← smul_smul, mul_comm, ← smul_smul]

Premises used: mul_assoc, smul_smul, mul_comm, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
a : R
ha : a ∈ (↑T : Set R)
u : ↥S
hu : ∏ a : ↥T, g a = g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) * u
⊢ (↑u : R) •
      (↑(g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha)) : R) • a ^ e (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) • m =
    0

Tactic:
smul_eq_zero_of_right u.1 (hg ⟨a, ha⟩)

Premises used: Subtype.mk, smul_eq_zero_of_right, Subtype.val
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
a : R
ha : a ∈ (↑T : Set R)
u : ↥S
hu : ∏ a : ↥T, g a = g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) * u
⊢ (↑u : R) •
      (↑(g (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha)) : R) • a ^ e (Subtype.mk (p := fun (x : R) ↦ x ∈ T) a ha) • m =
    0

Tactic:
exact smul_eq_zero_of_right u.1 (hg ⟨a, ha⟩)

Premises used: Subtype.mk, smul_eq_zero_of_right, Subtype.val
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
hr :
  Membership.mem (γ := Submodule R R)
    (Ideal.radical (colon (M := M) ⊥ {HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ a : ↥T, g a) : R) m})) r
⊢ ∃ (n : ℕ), (r ^ n * (↑(∏ a : ↥T, g a) : R)) • m = 0

Tactic:
simp only [Ideal.mem_radical_iff, mem_bot, mem_colon_singleton, smul_smul] at hr

Premises used: Submodule.mem_bot, smul_smul, Submodule.mem_colon_singleton, Ideal.mem_radical_iff
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
hr : ∃ (n : ℕ), (r ^ n * (↑(∏ a : ↥T, g a) : R)) • m = 0
refine_2 :
  ∀ (k : ℕ) (hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0),
    Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r

Tactic:
obtain ⟨k, hk⟩ := hr
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
rw :
  Membership.mem (γ := Ideal R)
    (Ideal.comap (F := R →+* R') (algebraMap R R') (Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})))
    (r ^ k * (↑(∏ a : ↥T, g a) : R))
⊢ Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (r ^ k * (↑(∏ a : ↥T, g a) : R))

Tactic:
rw [hx]
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
h :
  Membership.mem (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    (HPow.hPow (α := R') (β := ℕ) ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R') 1)
⊢ Membership.mem (γ := Ideal R)
    (Ideal.comap (F := R →+* R') (algebraMap R R') (Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})))
    (r ^ k * (↑(∏ a : ↥T, g a) : R))

Tactic:
use 1
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
h :
  Membership.mem.{u_2, u_2} (α := R') (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
h₁ :
  Membership.mem (γ := Submodule R' M') ⊥
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R') ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R')
      (IsLocalizedModule.mk' f m s))
h₂ : Membership.mem (γ := Submodule R' M') ⊥ ((r ^ k * (↑(∏ a : ↥T, g a) : R)) • IsLocalizedModule.mk' f m s)
h₃ : Membership.mem (γ := Submodule R' M') ⊥ (IsLocalizedModule.mk' f ((r ^ k * (↑(∏ a : ↥T, g a) : R)) • m) s)
h₄ : Membership.mem (γ := Submodule R' M') ⊥ (IsLocalizedModule.mk' f 0 s)
h₅ : Membership.mem (γ := Submodule R' M') ⊥ 0
⊢ Membership.mem (γ := Ideal R') (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
    (HPow.hPow (α := R') (β := ℕ) ((algebraMap R R' : (a : R) → R') (r ^ k * (↑(∏ a : ↥T, g a) : R)) : R') 1)

Tactic:
simp_rw [pow_one, mem_colon_singleton, algebraMap_smul, ← IsLocalizedModule.mk'_smul,
        hk, IsLocalizedModule.mk'_zero, mem_bot]

Premises used: Submodule.mem_bot, IsLocalizedModule.mk'_zero, algebraMap_smul, pow_one, IsLocalizedModule.mk'_smul, Submodule.mem_colon_singleton
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
⊢ Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (r ^ k * (↑(∏ a : ↥T, g a) : R))

Tactic:
have mem : r ^ k * (∏ a, g a).1 ∈ Ideal.comap (algebraMap R R') p := by
      rw [hx]
      use 1
      simp_rw [pow_one, mem_colon_singleton, algebraMap_smul, ← IsLocalizedModule.mk'_smul,
        hk, IsLocalizedModule.mk'_zero, mem_bot]
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
mem : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (r ^ k * (↑(∏ a : ↥T, g a) : R))
refine_2 : HPow.hPow (α := R') ((algebraMap R R' : (a : R) → R') r : R') k ∈ p
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) r

Tactic:
apply hp.mem_of_pow_mem k

Premises used: Ideal.IsPrime.mem_of_pow_mem
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
mem : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (r ^ k * (↑(∏ a : ↥T, g a) : R))
refine_2 : Membership.mem (α := R') p ((algebraMap R R' : (a : R) → R') (r ^ k) : R')
⊢ HPow.hPow (α := R') ((algebraMap R R' : (a : R) → R') r : R') k ∈ p

Tactic:
rw [← map_pow]

Premises used: map_pow
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
mem : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (r ^ k * (↑(∏ a : ↥T, g a) : R))
⊢ Membership.mem (α := R') p ((algebraMap R R' : (a : R) → R') (r ^ k) : R')

Tactic:
((hp.under R).mul_mem_iff_mem_or_mem.mp mem).resolve_right
      (Set.disjoint_left.mp ((IsLocalization.disjoint_under_iff S R' p).mpr hp.1) (∏ a, g a).2)

Premises used: Iff.mpr, Finset.univ, Set.Mem, Set.disjoint_left, setOf, Finset.prod, Set.preimage, Iff.mp, Or.resolve_right, Ideal.IsPrime.under, Ideal.IsPrime.ne_top', IsLocalization.disjoint_under_iff, Ideal.IsPrime.mul_mem_iff_mem_or_mem, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Eq (α := Ideal R) (Ideal.span (↑T : Set R)) (Ideal.comap (F := R →+* R') (algebraMap R R') p)
m : M
s : ↥S
hx : p = Ideal.radical (colon (M := M') ⊥ {IsLocalizedModule.mk' f m s})
e : (a : ↥T) → ℕ
g : (a : ↥T) → ↥S
hg : ∀ (a : ↥T), g a • (↑a : R) ^ e a • m = 0
r : R
k : ℕ
hk : (r ^ k * (↑(∏ a : ↥T, g a) : R)) • m = 0
mem : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') p) (r ^ k * (↑(∏ a : ↥T, g a) : R))
⊢ Membership.mem (α := R') p ((algebraMap R R' : (a : R) → R') (r ^ k) : R')

Tactic:
exact ((hp.under R).mul_mem_iff_mem_or_mem.mp mem).resolve_right
      (Set.disjoint_left.mp ((IsLocalization.disjoint_under_iff S R' p).mpr hp.1) (∏ a, g a).2)

Premises used: Iff.mpr, Finset.univ, Set.disjoint_left, Finset.prod, Iff.mp, Or.resolve_right, Ideal.IsPrime.under, Ideal.IsPrime.ne_top', IsLocalization.disjoint_under_iff, Ideal.IsPrime.mul_mem_iff_mem_or_mem, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
inst_10 : IsNoetherianRing R
h :
  ∀ (p : Ideal R'),
    Membership.mem (γ := Set (Ideal R'))
        (preimage (β := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R')) (associatedPrimes R M)) p ↔
      Membership.mem (γ := Set (Ideal R')) (associatedPrimes R' M') p
⊢ Eq (α := Set (Ideal R'))
    (preimage (β := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R')) (associatedPrimes R M))
    (associatedPrimes R' M')

Tactic:
ext p
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
inst_10 : IsNoetherianRing R
p : Ideal R'
⊢ Membership.mem (γ := Set (Ideal R'))
      (preimage (β := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R')) (associatedPrimes R M)) p ↔
    Membership.mem (γ := Set (Ideal R')) (associatedPrimes R' M') p

Tactic:
⟨mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule S f p,
    fun h ↦ comap_mem_associatedPrimes_of_mem_associatedPrimes_of_isLocalizedModule_of_fg S f p h
    ((isNoetherianRing_iff_ideal_fg R).mp ‹_› _)⟩

Premises used: Module.associatedPrimes.mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule, Algebra.algebraMap, isNoetherianRing_iff_ideal_fg, Iff.intro, Ideal.comap, Iff.mp, Module.associatedPrimes.comap_mem_associatedPrimes_of_mem_associatedPrimes_of_isLocalizedModule_of_fg
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
R' : Type u_2
inst_1 : CommRing R'
inst_2 : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
inst_8 : Module R' M'
inst_9 : IsScalarTower R R' M'
inst_10 : IsNoetherianRing R
p : Ideal R'
⊢ Membership.mem (γ := Set (Ideal R'))
      (preimage (β := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R')) (associatedPrimes R M)) p ↔
    Membership.mem (γ := Set (Ideal R')) (associatedPrimes R' M') p

Tactic:
exact ⟨mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule S f p,
    fun h ↦ comap_mem_associatedPrimes_of_mem_associatedPrimes_of_isLocalizedModule_of_fg S f p h
    ((isNoetherianRing_iff_ideal_fg R).mp ‹_› _)⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
⊢ p.IsPrime

Tactic:
have prime := hp.isPrime
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
⊢ Nontrivial (LocalizedModule p.primeCompl M)

Tactic:
simpa [← Module.mem_support_iff (p := ⟨p, prime⟩), Module.support_eq_zeroLocus] using hp.le

Premises used: Ideal.IsMinimalPrime.le, Module.mem_support_iff, Module.support_eq_zeroLocus
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
⊢ Nontrivial (LocalizedModule p.primeCompl M)

Tactic:
have : Nontrivial (LocalizedModule p.primeCompl M) := by
    simpa [← Module.mem_support_iff (p := ⟨p, prime⟩), Module.support_eq_zeroLocus] using hp.le
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
rcases :
  ∀ (q : Ideal Rₚ) (hq : Membership.mem (γ := Set (Ideal Rₚ)) (associatedPrimes Rₚ (LocalizedModule p.primeCompl M)) q),
    Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p

Tactic:
rcases associatedPrimes.nonempty Rₚ (LocalizedModule p.primeCompl M) with ⟨q, hq⟩

Premises used: LocalizedModule, associatedPrimes.nonempty, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
hq : Membership.mem (γ := Set (Ideal Rₚ)) (associatedPrimes Rₚ (LocalizedModule p.primeCompl M)) q
⊢ q.IsPrime

Tactic:
have q_prime : q.IsPrime := IsAssociatedPrime.isPrime hq