awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton M
hI : I.IsPrime
x : M
hx : I = Ideal.radical (colon (M := M) ⊥ {x})
⊢ False
have apply : I = ⊤
Tactic: apply hI.ne_top
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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
⊢ ∃ (P : Ideal R), IsAssociatedPrime P M ∧ colon (M := M) ⊥ {x} ≤ P
have simp : ∃ (P : Ideal R), (P.IsPrime ∧ ∃ (x : M), P = colon (M := M) ⊥ {x}) ∧ colon (M := M) ⊥ {x} ≤ P
Tactic: simp only [isAssociatedPrime_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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
⊢ ∃ (P : Ideal R), (P.IsPrime ∧ ∃ (x : M), P = colon (M := M) ⊥ {x}) ∧ colon (M := M) ⊥ {x} ≤ P
have obtain : ∀ (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}) ⊤),
  ∃ (P : Ideal R), (P.IsPrime ∧ ∃ (x : M), P = colon (M := M) ⊥ {x}) ∧ colon (M := M) ⊥ {x} ≤ P
Tactic: obtain ⟨P, ⟨l, h₁, y, rfl⟩, h₃⟩ :=
    set_has_maximal_iff_noetherian.mpr H
      { P | (⊥ : Submodule R M).colon {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ y : M, P = (⊥ : Submodule R M).colon {y} }
      ⟨_, rfl.le, by simpa, x, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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}) ⊤
⊢ ∃ (P : Ideal R), (P.IsPrime ∧ ∃ (x : M), P = colon (M := M) ⊥ {x}) ∧ colon (M := M) ⊥ {x} ≤ P
have refine : ∀ {x y_1 : R},
  Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) (x * y_1) →
    Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) x ∨ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) y_1
Tactic: refine ⟨_, ⟨⟨h₁, ?_⟩, y, rfl⟩, l⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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 (γ := Ideal R) (colon (M := M) ⊥ {y}) (a * b)
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) a ∨ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) b
have rw : a ∉ colon (M := M) ⊥ {y} → Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) b
Tactic: rw [or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
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 (γ := Ideal R) (colon (M := M) ⊥ {y}) (a * b)
ha : a ∉ colon (M := M) ⊥ {y}
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) b
have hab₁ : Membership.mem (γ := Submodule R M) ⊥ ((a * b) • y)
Tactic: rw [mem_colon_singleton] at ha hab
Cleared hypotheses: hab, ha
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
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 (γ := Ideal R) (colon (M := M) ⊥ {y}) (a * b)
ha : a ∉ colon (M := M) ⊥ {y}
hab₁ : Membership.mem (γ := Submodule R M) ⊥ ((a * b) • y)
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) b
have ha₁ : a • y ∉ ⊥
Tactic: rw [mem_colon_singleton] at ha hab
Cleared hypotheses: hab, ha
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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 ∉ ⊥
c : R
hc : Membership.mem (γ := Submodule R R) (colon (M := M) ⊥ {y}) c
⊢ Membership.mem (γ := Submodule R R) (colon (M := M) ⊥ {a • y}) c
have rw : ∀ (hc : c • y = 0), c • a • y = 0
Tactic: rw [mem_colon_singleton, mem_bot] at hc ⊢
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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 ∉ ⊥
c : R
hc : c • y = 0
⊢ c • a • y = 0
have rw : a • c • y = 0
Tactic: rw [smul_comm, hc, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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 ∉ ⊥
c : R
hc : c • y = 0
rw : a • c • y = 0
⊢ c • a • y = 0
have rw₁ : HSMul.hSMul (β := M) a 0 = 0
Tactic: rw [smul_comm, hc, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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 ∉ ⊥
c : R
hc : c • y = 0
rw : a • c • y = 0
rw₁ : HSMul.hSMul (β := M) a 0 = 0
⊢ c • a • y = 0
have rw₂ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [smul_comm, hc, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
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 ∉ ⊥
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) b
have H₁ : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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})
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) b
have rwa : Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {a • y}) b
Tactic: rwa [H₁.eq_of_not_lt (h₃ _ ⟨l.trans H₁, by simpa, _, rfl⟩),
    mem_colon_singleton, smul_comm, smul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) b
have rwa₁ : Membership.mem (γ := Submodule R M) ⊥ (b • a • y)
Tactic: rwa [H₁.eq_of_not_lt (h₃ _ ⟨l.trans H₁, by simpa, _, rfl⟩),
    mem_colon_singleton, smul_comm, smul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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)
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) b
have rwa₂ : Membership.mem (γ := Submodule R M) ⊥ (a • b • y)
Tactic: rwa [H₁.eq_of_not_lt (h₃ _ ⟨l.trans H₁, by simpa, _, rfl⟩),
    mem_colon_singleton, smul_comm, smul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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})
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M ∪ associatedPrimes R M'') p
have 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
Tactic: by_cases! h : ∃ a ∈ p.primeCompl, ∃ y : M, ∃ k, f y = a ^ k • x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M ∪ associatedPrimes R M'') p
have 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
Tactic: by_cases! h : ∃ a ∈ p.primeCompl, ∃ y : M, ∃ k, f y = a ^ k • x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M ∪ associatedPrimes R M'') p
have 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
Tactic: obtain ⟨a, ha, y, k, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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 ∪ associatedPrimes R M'') p
have pos : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
Tactic: left
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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
have pos : ∀ (b : R) (hb : b ∈ p), Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
Tactic: refine ⟨‹_›, y, le_antisymm (fun b hb ↦ ?_) (fun b ⟨n, hb⟩ ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
have 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
Tactic: refine ⟨‹_›, y, le_antisymm (fun b hb ↦ ?_) (fun b ⟨n, hb⟩ ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
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) ⊥ {y})) b
have hb₁ : Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M') ⊥ {x})) b
Tactic: rw [hx] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
have 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
Tactic: obtain ⟨n, hb⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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)
⊢ Membership.mem (γ := Submodule R R) (Ideal.radical (colon (M := M) ⊥ {y})) b
have h₁ : Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) (b ^ n)
Tactic: use n
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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)
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) (b ^ n)
have h₁ : ∀ (hb : b ^ n • x = 0), b ^ n • y = 0
Tactic: rw [mem_colon_singleton, mem_bot] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
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
⊢ b ^ n • y = 0
have h₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b ^ n • y) : M') ((f : (a : M) → M') 0 : M')
Tactic: apply_fun _ using hf