awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : Ring.KrullDimLE 0 R
eq : Eq (α := Ideal R) (Ring.jacobson R) (nilradical R)
Spec : Set (Ideal R) := {I : Ideal R | I.IsPrime}
this_1 : Finite.{u_3 + 1} (↑Spec : Type u_3)
this_2 : ∀ (I : (↑Spec : Type u_3)), (↑I : Ideal R).IsPrime
this : ∀ (I : (↑Spec : Type u_3)), IsSemisimpleRing.{u_3} (R ⧸ (↑I : Ideal R))
rw :
  IsSemisimpleRing.{u_3}
    (HasQuotient.Quotient R (B := Ideal R) (⨅ (a : (↑{J : Ideal R | J.IsPrime} : Type u_3)), (↑a : Ideal R)))
⊢ IsSemisimpleRing.{u_3} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))

Tactic:
rw [eq, nilradical_eq_sInf, sInf_eq_iInf']

Premises used: sInf_eq_iInf', nilradical_eq_sInf
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : Ring.KrullDimLE 0 R
eq : Eq (α := Ideal R) (Ring.jacobson R) (nilradical R)
Spec : Set (Ideal R) := {I : Ideal R | I.IsPrime}
this_1 : Finite.{u_3 + 1} (↑Spec : Type u_3)
this_2 : ∀ (I : (↑Spec : Type u_3)), (↑I : Ideal R).IsPrime
this : ∀ (I : (↑Spec : Type u_3)), IsSemisimpleRing.{u_3} (R ⧸ (↑I : Ideal R))
⊢ IsSemisimpleRing.{u_3}
    (HasQuotient.Quotient R (B := Ideal R) (⨅ (a : (↑{J : Ideal R | J.IsPrime} : Type u_3)), (↑a : Ideal R)))

Tactic:
(Ideal.quotientInfRingEquivPiQuotient _ fun I J ne ↦
      Ideal.isCoprime_of_isMaximal <| Subtype.coe_ne_coe.mpr ne).symm.isSemisimpleRing

Premises used: Iff.mpr, RingEquiv.isSemisimpleRing, Ideal.quotientInfRingEquivPiQuotient, Ideal.isCoprime_of_isMaximal, RingEquiv.symm, Subtype.coe_ne_coe
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : Ring.KrullDimLE 0 R
eq : Eq (α := Ideal R) (Ring.jacobson R) (nilradical R)
Spec : Set (Ideal R) := {I : Ideal R | I.IsPrime}
this_1 : Finite.{u_3 + 1} (↑Spec : Type u_3)
this_2 : ∀ (I : (↑Spec : Type u_3)), (↑I : Ideal R).IsPrime
this : ∀ (I : (↑Spec : Type u_3)), IsSemisimpleRing.{u_3} (R ⧸ (↑I : Ideal R))
⊢ IsSemisimpleRing.{u_3}
    (HasQuotient.Quotient R (B := Ideal R) (⨅ (a : (↑{J : Ideal R | J.IsPrime} : Type u_3)), (↑a : Ideal R)))

Tactic:
exact (Ideal.quotientInfRingEquivPiQuotient _ fun I J ne ↦
      Ideal.isCoprime_of_isMaximal <| Subtype.coe_ne_coe.mpr ne).symm.isSemisimpleRing

Premises used: Iff.mpr, RingEquiv.isSemisimpleRing, Ideal.quotientInfRingEquivPiQuotient, Ideal.isCoprime_of_isMaximal, RingEquiv.symm, Subtype.coe_ne_coe
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_3
inst : CommRing R
⊢ IsArtinianRing R ↔ IsNoetherianRing R ∧ Ring.KrullDimLE 0 R

Tactic:
⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨h, _⟩ ↦ h.isArtinianRing_of_krullDimLE_zero⟩

Premises used: _private.0.isArtinianRing_iff_isNoetherianRing_krullDimLE_zero.match_1, IsArtinianRing, inferInstance, IsNoetherianRing.isArtinianRing_of_krullDimLE_zero, And.intro, Iff.intro
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
rwa : IsNoetherianRing R ∧ Ring.KrullDimLE 0 R ↔ Ring.KrullDimLE 0 R
rwa₁ : Ring.KrullDimLE 0 R ↔ Ring.KrullDimLE 0 R
rwa₂ : IsNoetherianRing R
rwa₃ : Ring.KrullDimLE 0 R ↔ Ring.KrullDimLE 0 R
rwa₄ rwa₅ rwa₆ : IsNoetherianRing R
⊢ IsArtinianRing R ↔ Ring.KrullDimLE 0 R

Tactic:
rwa [isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, and_iff_right]

Premises used: isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, and_iff_right
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
rw : LE.le (α := Ideal R) (nilradical R) (IsLocalRing.maximalIdeal R)
⊢ IsArtinianRing R ↔ IsNilpotent (R := Ideal R) (IsLocalRing.maximalIdeal R)

Tactic:
rw [isArtinianRing_iff_krullDimLE_zero,
    Ideal.FG.isNilpotent_iff_le_nilradical (IsNoetherian.noetherian _),
    ← and_iff_left (a := Ring.KrullDimLE 0 R) ‹IsLocalRing R›,
    (Ring.krullDimLE_zero_and_isLocalRing_tfae R).out 0 3 rfl rfl,
    IsLocalRing.isMaximal_iff, le_antisymm_iff, and_iff_right]

Premises used: Ring.krullDimLE_zero_and_isLocalRing_tfae, and_iff_left, IsNoetherian.noetherian, and_iff_right, List.TFAE.out, le_antisymm_iff, Ideal.FG.isNilpotent_iff_le_nilradical, IsLocalRing.isMaximal_iff, OfNat.ofNat, isArtinianRing_iff_krullDimLE_zero, rfl
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ Ne (α := Ideal R) (nilradical R) ⊤

Tactic:
simp [nilradical, Ideal.radical_eq_top]

Premises used: Ideal.radical_eq_top, nilradical
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ LE.le (α := Ideal R) (nilradical R) (IsLocalRing.maximalIdeal R)

Tactic:
exact IsLocalRing.le_maximalIdeal (by simp [nilradical, Ideal.radical_eq_top])

Premises used: IsLocalRing.le_maximalIdeal
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
I : Ideal R
⊢ N.IsAssociatedPrime I ↔ I.IsPrime ∧ ∃ (x : M), I = (N.colon {x}).radical

Tactic:
⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩

Premises used: Submodule.IsAssociatedPrime.mk, And.right, And.left, And.intro, Iff.intro, Submodule.IsAssociatedPrime.eq_radical_colon, Submodule.IsAssociatedPrime.toIsPrime
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
I : Ideal R
inst_3 : IsNoetherianRing R
mp : N.IsAssociatedPrime I → I.IsPrime ∧ ∃ (x : M), I = N.colon {x}
mpr : (I.IsPrime ∧ ∃ (x : M), I = N.colon {x}) → N.IsAssociatedPrime I
⊢ N.IsAssociatedPrime I ↔ I.IsPrime ∧ ∃ (x : M), I = N.colon {x}

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsNoetherianRing R
x : M
hx : (N.colon {x}).radical.IsPrime
⊢ (N.colon {x}).radical.IsPrime ∧ ∃ (x_1 : M), (N.colon {x}).radical = N.colon {x_1}

Tactic:
⟨hx, exists_eq_colon_of_mem_minimalPrimes (x := x) ?_⟩

Premises used: And.intro, Submodule.exists_eq_colon_of_mem_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsNoetherianRing R
x : M
hx : (N.colon {x}).radical.IsPrime
mp : (N.colon {x}).radical ∈ (N.colon {x}).minimalPrimes
⊢ (N.colon {x}).radical.IsPrime ∧ ∃ (x_1 : M), (N.colon {x}).radical = N.colon {x_1}

Tactic:
refine ⟨hx, exists_eq_colon_of_mem_minimalPrimes (x := x) ?_⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsNoetherianRing R
x : M
hx : (N.colon {x}).radical.IsPrime
mp : (N.colon {x}).radical ∈ (N.colon {x}).radical.minimalPrimes
mp₁ : Membership.mem (γ := Set (Ideal R)) {(N.colon {x}).radical} (N.colon {x}).radical
mp₂ mp₃ : (N.colon {x}).radical = (N.colon {x}).radical
⊢ (N.colon {x}).radical ∈ (N.colon {x}).minimalPrimes

Tactic:
rw [← Ideal.radical_minimalPrimes, Ideal.minimalPrimes_eq_subsingleton_self,
      Set.mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Ideal.minimalPrimes_eq_subsingleton_self, Ideal.radical_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsNoetherianRing R
x : M
hx : (N.colon {x}).IsPrime
⊢ N.IsAssociatedPrime (N.colon {x})

Tactic:
⟨hx, x, hx.radical.symm⟩

Premises used: Submodule.IsAssociatedPrime.mk, Exists.intro, Eq.symm, Ideal.IsPrime.radical
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsNoetherianRing R
x : M
hx : (N.colon {x}).IsPrime
⊢ N.IsAssociatedPrime (N.colon {x})

Tactic:
exact ⟨hx, x, hx.radical.symm⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
I_1 : Ideal R
x : M
I : (↑N.associatedPrimes : Type u_1)
⊢ (↑I : Ideal R).IsPrime

Tactic:
I.2.1

Premises used: Subtype.property, Submodule.IsAssociatedPrime.toIsPrime
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
I : Ideal R
⊢ I ∈ N.associatedPrimes ↔ N.IsAssociatedPrime I

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Submodule.associatedPrimes
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) I ↔ IsAssociatedPrime I M

Tactic:
Iff.rfl

Premises used: IsAssociatedPrime, Set.Mem, Iff.rfl, setOf, associatedPrimes
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : IsAssociatedPrime I M
⊢ I.IsPrime

Tactic:
h.1

Premises used: Submodule.IsAssociatedPrime.toIsPrime
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I_1 J : Ideal 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'
I : (↑(associatedPrimes R M) : Type u_1)
⊢ (↑I : Ideal R).IsPrime

Tactic:
I.2.1

Premises used: Subtype.property, Submodule.IsAssociatedPrime.toIsPrime
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
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 : IsNoetherianRing R
⊢ IsAssociatedPrime I M ↔ I.IsPrime ∧ ∃ (x : M), I = colon (M := M) ⊥ {x}

Tactic:
(⊥ : Submodule R M).isAssociatedPrime_iff

Premises used: IsAssociatedPrime, Submodule.isAssociatedPrime_iff
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal 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'
h : IsAssociatedPrime I M
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
obtain :
  ∀ (x : M) (h : IsAssociatedPrime.{u_1, u_2} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M),
    IsAssociatedPrime.{u_1, u_3} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M'
⊢ IsAssociatedPrime I M'

Tactic:
obtain ⟨x, rfl⟩ := h.2

Premises used: Submodule.IsAssociatedPrime.eq_radical_colon, 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')
x : M
h : IsAssociatedPrime.{u_1, u_2} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M
⊢ IsAssociatedPrime.{u_1, u_3} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M'

Tactic:
⟨h.1, ⟨f x, ?_⟩⟩

Premises used: IsAssociatedPrime, Submodule.IsAssociatedPrime.mk, Exists.intro, DFunLike.coe, Submodule.IsAssociatedPrime.toIsPrime
-- 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')
x : M
h : IsAssociatedPrime.{u_1, u_2} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M
refine :
  Eq.{u_1 + 1} (α := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x}))
    (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
⊢ IsAssociatedPrime.{u_1, u_3} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M'

Tactic:
refine ⟨h.1, ⟨f x, ?_⟩⟩
-- 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')
x : M
h : IsAssociatedPrime.{u_1, u_2} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M
h₁ :
  ∀ (r : R),
    Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) r ↔
      Membership.mem (γ := Ideal R)
        (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M')))) r
⊢ Eq.{u_1 + 1} (α := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x}))
    (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))

Tactic:
ext r
-- 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')
x : M
h : IsAssociatedPrime.{u_1, u_2} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M
r : R
h₁ :
  (∃ (n : ℕ), Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {x}) (r ^ n)) ↔
    ∃ (n : ℕ),
      Membership.mem (γ := Ideal R) (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))) (r ^ n)
h₂ :
  (∃ (n : ℕ), Membership.mem (γ := Submodule R M) ⊥ (r ^ n • x)) ↔
    ∃ (n : ℕ), Membership.mem (γ := Submodule R M') ⊥ (HSMul.hSMul (β := M') (r ^ n) ((f : (a : M) → M') x : M'))
h₃ : (∃ (n : ℕ), r ^ n • x = 0) ↔ ∃ (n : ℕ), HSMul.hSMul (β := M') (r ^ n) ((f : (a : M) → M') x : M') = 0
h₄ : (∃ (n : ℕ), r ^ n • x = 0) ↔ ∃ (n : ℕ), Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (r ^ n • x) : M') (0 : M')
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) r ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
      r

Tactic:
simp_rw [Ideal.mem_radical_iff, mem_colon_singleton, mem_bot, ← map_smul, map_eq_zero_iff f hf]

Premises used: Submodule.mem_bot, map_eq_zero_iff, Submodule.mem_colon_singleton, Ideal.mem_radical_iff, map_smul
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal 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'
l : M ≃ₗ[R] M'
⊢ IsAssociatedPrime I M ↔ IsAssociatedPrime I M'

Tactic:
⟨fun h => h.map_of_injective l l.injective,
    fun h => h.map_of_injective l.symm l.symm.injective⟩

Premises used: IsAssociatedPrime.map_of_injective, Iff.intro
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
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})
apply : I = ⊤
⊢ False

Tactic:
apply hI.ne_top

Premises used: Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
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})
⊢ I = ⊤

Tactic:
simp [hx, Subsingleton.elim x 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- 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
simp : ∃ (P : Ideal R), (P.IsPrime ∧ ∃ (x : M), P = colon (M := M) ⊥ {x}) ∧ colon (M := M) ⊥ {x} ≤ P
⊢ ∃ (P : Ideal R), IsAssociatedPrime P M ∧ colon (M := M) ⊥ {x} ≤ P

Tactic:
simp only [isAssociatedPrime_iff]

Premises used: isAssociatedPrime_iff
-- 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
⊢ Ne.{u_1 + 1} (α := Submodule R R) (colon (M := M) ⊥ {x}) ⊤

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
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
⊢ ∃ (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⟩

Premises used: Iff.mpr, Submodule.colon, setOf, Exists, Eq.le, Ne, Bot.bot, LE.le, And, And.intro, Exists.intro, set_has_maximal_iff_noetherian, Top.top, Singleton.singleton, Eq, 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
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

Tactic:
⟨_, ⟨⟨h₁, ?_⟩, y, rfl⟩, l⟩

Premises used: And.intro, Exists.intro, Ideal.IsPrime.mk, 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
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}) ⊤
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
⊢ ∃ (P : Ideal R), (P.IsPrime ∧ ∃ (x : M), P = colon (M := M) ⊥ {x}) ∧ colon (M := M) ⊥ {x} ≤ P

Tactic:
refine ⟨_, ⟨⟨h₁, ?_⟩, y, rfl⟩, l⟩
-- 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 (γ := Ideal R) (colon (M := M) ⊥ {y}) (a * b)
rw : a ∉ colon (M := M) ⊥ {y} → Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) b
⊢ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) a ∨ Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {y}) b

Tactic:
rw [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_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
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 (γ := Submodule R M) ⊥ ((a * b) • y)

Tactic:
rw [mem_colon_singleton] at ha hab

Premises used: 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
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)
⊢ a • y ∉ ⊥

Tactic:
rw [mem_colon_singleton] at ha hab

Premises used: 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
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
rw : ∀ (hc : c • y = 0), c • a • y = 0
⊢ Membership.mem (γ := Submodule R R) (colon (M := M) ⊥ {a • y}) c

Tactic:
rw [mem_colon_singleton, mem_bot] at hc ⊢

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
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
rw₂ rw₃ : Eq.{u_2 + 1} (α := M) 0 0
⊢ c • a • y = 0

Tactic:
rw [smul_comm, hc, smul_zero]

Premises used: smul_zero, SMulCommClass.smul_comm