awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ :
  ∀ (I : Submodule R R),
    Membership.mem (γ := Set (Submodule R R))
        {P : Submodule R R | colon (M := M) ⊥ {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ (y : M), P = colon (M := M) ⊥ {y}} I →
      ¬colon (M := M) ⊥ {y} < I
l : LE.le.{u_1} (α := Ideal R) (colon (M := M) ⊥ {x}) (colon (M := M) ⊥ {y})
h₁ : Ne.{u_1 + 1} (α := Submodule R R) (colon (M := M) ⊥ {y}) ⊤
a b : R
hab : Membership.mem (γ := Submodule R M) ⊥ ((a * b) • y)
ha : a • y ∉ ⊥
⊢ LE.le.{u_1} (α := Ideal R) (colon (M := M) ⊥ {y}) (colon (M := M) ⊥ {a • y})

Tactic:
have H₁ : (⊥ : Submodule R M).colon {y} ≤ (⊥ : Submodule R M).colon {a • y} := by
    intro c hc
    rw [mem_colon_singleton, mem_bot] at hc ⊢
    rw [smul_comm, hc, smul_zero]
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ :
  ∀ (I : Submodule R R),
    Membership.mem (γ := Set (Submodule R R))
        {P : Submodule R R | colon (M := M) ⊥ {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ (y : M), P = colon (M := M) ⊥ {y}} I →
      ¬colon (M := M) ⊥ {y} < I
l : LE.le.{u_1} (α := Ideal R) (colon (M := M) ⊥ {x}) (colon (M := M) ⊥ {y})
h₁ : Ne.{u_1 + 1} (α := Submodule R R) (colon (M := M) ⊥ {y}) ⊤
a b : R
hab : Membership.mem (γ := Submodule R M) ⊥ ((a * b) • y)
ha : a • y ∉ ⊥
H₁ : LE.le.{u_1} (α := Ideal R) (colon (M := M) ⊥ {y}) (colon (M := M) ⊥ {a • y})
⊢ Ne.{u_1 + 1} (α := Submodule R R) (colon (M := M) ⊥ {a • y}) ⊤

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ :
  ∀ (I : Submodule R R),
    Membership.mem (γ := Set (Submodule R R))
        {P : Submodule R R | colon (M := M) ⊥ {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ (y : M), P = colon (M := M) ⊥ {y}} I →
      ¬colon (M := M) ⊥ {y} < I
l : LE.le.{u_1} (α := Ideal R) (colon (M := M) ⊥ {x}) (colon (M := M) ⊥ {y})
h₁ : Ne.{u_1 + 1} (α := Submodule R R) (colon (M := M) ⊥ {y}) ⊤
a b : R
hab : Membership.mem (γ := Submodule R M) ⊥ ((a * b) • y)
ha : a • y ∉ ⊥
H₁ : LE.le.{u_1} (α := Ideal R) (colon (M := M) ⊥ {y}) (colon (M := M) ⊥ {a • y})
rwa : Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {a • y}) b
rwa₁ : Membership.mem (γ := Submodule R M) ⊥ (b • a • y)
rwa₂ : Membership.mem (γ := Submodule R M) ⊥ (a • b • y)
rwa₃ rwa₄ rwa₅ rwa₆ : Membership.mem (γ := Submodule R M) ⊥ ((a * b) • y)
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) b

Tactic:
rwa [H₁.eq_of_not_lt (h₃ _ ⟨l.trans H₁, by simpa, _, rfl⟩),
    mem_colon_singleton, smul_comm, smul_smul]

Premises used: smul_smul, LE.le.eq_of_not_lt, And.intro, Exists.intro, Submodule.mem_colon_singleton, LE.le.trans, SMulCommClass.smul_comm, rfl
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ Subset (α := Set (Ideal R)) (associatedPrimes R M) (associatedPrimes R M')

Tactic:
fun _I h => h.map_of_injective f hf

Premises used: IsAssociatedPrime, Set.Mem, setOf, IsAssociatedPrime.map_of_injective, Set.Subset, associatedPrimes
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
pos :
  ∀ (h : ∃ a ∈ p.primeCompl, ∃ (y : M) (k : ℕ), (f : (a : M) → M') y = a ^ k • x),
    Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M ∪ associatedPrimes R M'') p
neg :
  ∀ (h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x),
    Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M ∪ associatedPrimes R M'') p
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M ∪ associatedPrimes R M'') p

Tactic:
by_cases! h : ∃ a ∈ p.primeCompl, ∃ y : M, ∃ k, f y = a ^ k • x

Premises used: Ideal.primeCompl
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∃ a ∈ p.primeCompl, ∃ (y : M) (k : ℕ), (f : (a : M) → M') y = a ^ k • x
pos :
  ∀ (a : R) (ha : a ∈ p.primeCompl) (y : M) (k : ℕ) (h : (f : (a : M) → M') y = a ^ k • x),
    Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M ∪ associatedPrimes R M'') p
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M ∪ associatedPrimes R M'') p

Tactic:
obtain ⟨a, ha, y, k, h⟩ := h
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
pos : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M ∪ associatedPrimes R M'') p

Tactic:
left
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p

Tactic:
⟨‹_›, y, le_antisymm (fun b hb ↦ ?_) (fun b ⟨n, hb⟩ ↦ ?_)⟩

Premises used: IsAssociatedPrime, Submodule.IsAssociatedPrime.mk, Set.Mem, setOf, _private.0.associatedPrimes.subset_union_of_exact.match_1, Membership.mem, le_antisymm, associatedPrimes, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
pos : ∀ (b : R) (hb : b ∈ p), Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
pos₁ :
  ∀ (b : R),
    Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b →
      ∀ (n : ℕ) (hb : Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) (b ^ n)), b ∈ p
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p

Tactic:
refine ⟨‹_›, y, le_antisymm (fun b hb ↦ ?_) (fun b ⟨n, hb⟩ ↦ ?_)⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
hb : b ∈ p
⊢ Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b

Tactic:
rw [hx] at hb
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
hb : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b
pos :
  ∀ (n : ℕ) (hb : Membership.mem (γ := Ideal R) (colon (M := M') ⊥ {x}) (b ^ n)),
    Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
⊢ Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b

Tactic:
obtain ⟨n, hb⟩ := hb
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
n : ℕ
hb : Membership.mem (γ := Ideal R) (colon (M := M') ⊥ {x}) (b ^ n)
h₁ : Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) (b ^ n)
⊢ Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b

Tactic:
use n
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
n : ℕ
hb : Membership.mem (γ := Ideal R) (colon (M := M') ⊥ {x}) (b ^ n)
h₁ : ∀ (hb : b ^ n • x = 0), b ^ n • y = 0
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) (b ^ n)

Tactic:
rw [mem_colon_singleton, mem_bot] at hb ⊢

Premises used: Submodule.mem_bot, Submodule.mem_colon_singleton
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
n : ℕ
hb : b ^ n • x = 0
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')

Tactic:
hf
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
n : ℕ
hb : b ^ n • x = 0
h₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')
⊢ b ^ n • y = 0

Tactic:
apply_fun _ using hf
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
n : ℕ
hb : b ^ n • x = 0
h₁ : HSMul.hSMul (β := M') (b ^ n) ((f : (a : M) → M') y : M') = (f : (a : M) → M') 0
h₂ : b ^ n • a ^ k • x = (f : (a : M) → M') 0
h₃ : a ^ k • b ^ n • x = (f : (a : M) → M') 0
h₄ : HSMul.hSMul (β := M') (a ^ k) 0 = (f : (a : M) → M') 0
h₅ : Eq.{u_3 + 1} (α := M') (0 : M') ((f : (a : M) → M') 0 : M')
h₆ h₇ : Eq.{u_3 + 1} (α := M') 0 0
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')

Tactic:
rw [map_smul, h, smul_comm, hb, smul_zero, map_zero]

Premises used: smul_zero, map_zero, SMulCommClass.smul_comm, map_smul
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
h_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
n : ℕ
hb : Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) (b ^ n)
⊢ b ^ n • y = 0

Tactic:
rw [mem_colon_singleton, mem_bot] at hb

Premises used: Submodule.mem_bot, Submodule.mem_colon_singleton
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
h_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
n : ℕ
hb : b ^ n • y = 0
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')

Tactic:
apply_fun f at hb
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
h_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
n : ℕ
hb : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')
⊢ Membership.mem (γ := Ideal R) (colon (M := M') ⊥ {x}) (b ^ n * a ^ k)

Tactic:
rw [map_smul, map_zero, h, ← mul_smul, ← mem_bot R, ← mem_colon_singleton] at hb

Premises used: Submodule.mem_bot, map_zero, Submodule.mem_colon_singleton, SemigroupAction.mul_smul, map_smul
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
h_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
n : ℕ
hb : Membership.mem (γ := Ideal R) (colon (M := M') ⊥ {x}) (b ^ n * a ^ k)
⊢ b ^ n * a ^ k ∈ p

Tactic:
replace hb := hx.ge (Ideal.le_radical hb)
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
h_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
n : ℕ
hb : b ^ n * a ^ k ∈ p
pos : ∀ (hb : ¬b ∈ p), b ^ n * a ^ k ∉ p
⊢ b ∈ p

Tactic:
contrapose hb
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
h_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
n : ℕ
hb : ¬b ∈ p
⊢ b ^ n * a ^ k ∉ p

Tactic:
p.primeCompl.mul_mem (p.primeCompl.pow_mem hb n) (p.primeCompl.pow_mem ha k)

Premises used: Submonoid.pow_mem, Submonoid.mul_mem, Set.Mem, setOf, Ideal.primeCompl, Not
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : (f : (a : M) → M') y = a ^ k • x
b : R
h_1 : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
n : ℕ
hb : ¬b ∈ p
⊢ b ^ n * a ^ k ∉ p

Tactic:
exact p.primeCompl.mul_mem (p.primeCompl.pow_mem hb n) (p.primeCompl.pow_mem ha k)

Premises used: Submonoid.pow_mem, Submonoid.mul_mem, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
neg : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M'') p
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M ∪ associatedPrimes R M'') p

Tactic:
right
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : Function.Exact.{u_2, u_3, u_4} (M := M) (N := M') (P := M'') (⇑f : (a : M) → M') (⇑g : (a : M') → M'')
p : Ideal R
toIsPrime : p.IsPrime
x : M'
hx : p = Ideal.radical (colon (M := M') ⊥ {x})
h : ∀ (a : R) (_ : a ∈ p.primeCompl) (y : M) (k : ℕ), (f : (a : M) → M') y ≠ a ^ k • x
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M'') p

Tactic:
⟨‹_›, g x, le_antisymm (fun b hb ↦ ?_) (fun b ⟨n, hb⟩ ↦ ?_)⟩

Premises used: IsAssociatedPrime, _private.0.associatedPrimes.subset_union_of_exact.match_2, Submodule.IsAssociatedPrime.mk, Set.Mem, setOf, Membership.mem, le_antisymm, associatedPrimes, Exists.intro, DFunLike.coe