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
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton M
⊢ Eq (α := Set (Ideal R)) (associatedPrimes R M) ∅
have h : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) x ↔ Membership.mem (γ := Set (Ideal R)) ∅ x
Tactic: ext
-- 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
inst_3 : Subsingleton M
x : Ideal R
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) x ↔ Membership.mem (γ := Set (Ideal R)) ∅ x
have h : x ∉ associatedPrimes R M
Tactic: simp only [Set.mem_empty_iff_false, iff_false]
-- 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
inst_3 : IsNoetherianRing R
inst_4 : Nontrivial M
⊢ Set.Nonempty (α := Ideal R) (associatedPrimes R M)
have obtain : ∀ (x : M) (hx : x ≠ 0), Set.Nonempty (α := Ideal R) (associatedPrimes R M)
Tactic: obtain ⟨x, hx⟩ := exists_ne (0 : M)
-- 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
inst_3 : IsNoetherianRing R
inst_4 : Nontrivial M
x : M
hx : x ≠ 0
⊢ Set.Nonempty (α := Ideal R) (associatedPrimes R M)
have obtain : ∀ (P : Ideal R) (hP : IsAssociatedPrime P M),
  colon (M := M) ⊥ {x} ≤ P → Set.Nonempty (α := Ideal R) (associatedPrimes R M)
Tactic: obtain ⟨P, hP, _⟩ := exists_le_isAssociatedPrime_of_isNoetherianRing R x hx
-- 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
inst_3 : IsNoetherianRing R
⊢ Eq.{u_1 + 1} (α := Set R)
    (⋃ (p : Ideal R), ⋃ (_ : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p), (↑p : Set R))
    {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}
have simp : Eq.{u_1 + 1} (α := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R))
  {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}
Tactic: simp only [AssociatedPrimes.mem_iff, 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
inst_3 : IsNoetherianRing R
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R))
    {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}
have refine_1 : ∀ (i : Ideal R) (j : i.IsPrime ∧ ∃ (x : M), i = colon (M := M) ⊥ {x}),
  (↑i : Set R) ⊆ {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}
Tactic: refine subset_antisymm (Set.iUnion₂_subset ?_) ?_
-- 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
inst_3 : IsNoetherianRing R
refine_1 :
  ∀ (i : Ideal R) (j : i.IsPrime ∧ ∃ (x : M), i = colon (M := M) ⊥ {x}),
    (↑i : Set R) ⊆ {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R))
    {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}
have refine_2 : Subset.{u_1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}
  (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R))
Tactic: refine subset_antisymm (Set.iUnion₂_subset ?_) ?_
-- 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
inst_3 : IsNoetherianRing R
r : R
⊢ Membership.mem (γ := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} r →
    Membership.mem (γ := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R))
      r
have refine_2 : ∀ (x : M) (h : x ≠ 0) (h' : r • x = 0),
  Membership.mem (γ := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R)) r
Tactic: ⟨x, h, 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
inst_3 : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
⊢ Membership.mem (γ := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R)) r
have refine_2 : ∀ (P : Ideal R) (hP : IsAssociatedPrime P M) (hx : colon (M := M) ⊥ {x} ≤ P),
  Membership.mem (γ := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R)) r
Tactic: obtain ⟨P, hP, hx⟩ := exists_le_isAssociatedPrime_of_isNoetherianRing R x h
-- 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
inst_3 : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
P : Ideal R
hP : IsAssociatedPrime P M
hx : colon (M := M) ⊥ {x} ≤ P
⊢ Membership.mem (γ := Set R) (⋃ (p : Ideal R), ⋃ (_ : p.IsPrime ∧ ∃ (x : M), p = colon (M := M) ⊥ {x}), (↑p : Set R)) r
have hP₁ : P.IsPrime ∧ ∃ (x : M), P = colon (M := M) ⊥ {x}
Tactic: rw [isAssociatedPrime_iff] at hP
Cleared hypotheses: hP, hx
-- 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
inst_3 : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
P : Ideal R
hP : P.IsPrime ∧ ∃ (x : M), P = colon (M := M) ⊥ {x}
hx : colon (M := M) ⊥ {x} ≤ P
⊢ Membership.mem (γ := Submodule R R) (colon (M := M) ⊥ {x}) r
have rwa : Membership.mem (γ := Submodule R M) ⊥ (r • x)
Tactic: rwa [mem_colon_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsNoetherianRing R
⊢ {r : R | ∃ (x : R), x ≠ 0 ∧ r • x = 0} = (↑(nonZeroDivisors R) : Set R)ᶜ
have h : ∀ (x : R), Membership.mem (γ := Set R) {r : R | ∃ (x : R), x ≠ 0 ∧ r • x = 0} x ↔ x ∈ (↑(nonZeroDivisors R) : Set R)ᶜ
Tactic: ext
-- 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
h : IsAssociatedPrime I M
⊢ annihilator.{u_1, u_2} (M := M) ⊤ ≤ I
have obtain : ∀ (x : M) (hI : Ideal.IsPrime.{u_1} (α := R) (Ideal.radical (colon (M := M) ⊥ {x}))),
  LE.le.{u_1} (α := Ideal R) (annihilator.{u_1, u_2} (M := M) ⊤) (Ideal.radical (colon (M := M) ⊥ {x}))
Tactic: obtain ⟨hI, x, rfl⟩ := h
Cleared hypotheses: I, 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
x : M
hI : Ideal.IsPrime.{u_1} (α := R) (Ideal.radical (colon (M := M) ⊥ {x}))
⊢ LE.le.{u_1} (α := Ideal R) (annihilator.{u_1, u_2} (M := M) ⊤) (Ideal.radical (colon (M := M) ⊥ {x}))
have rw : LE.le (α := Ideal R) (annihilator.{u_1, u_2} (M := M) ⊤) (Ideal.radical (annihilator (M := M) (R ∙ x)))
Tactic: rw [bot_colon']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
⊢ IsAssociatedPrime I M ↔
    I.IsPrime ∧
      ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
have rw : I.IsPrime →
  ((∃ (x : M), I = colon (M := M) ⊥ {x}) ↔
    ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M))
Tactic: rw [isAssociatedPrime_iff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
⊢ I.IsPrime →
    ((∃ (x : M), I = colon (M := M) ⊥ {x}) ↔
      ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M))
have refine_1 : I.IsPrime →
  (∃ (x : M), I = colon (M := M) ⊥ {x}) →
    ∀ (x : M) (h : I = colon (M := M) ⊥ {x}),
      ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
Tactic: refine fun _ ↦ ⟨fun ⟨x, h⟩ ↦ ?_, fun ⟨f, h⟩ ↦ ⟨(f ∘ₗ mkQ I) 1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
refine_1 :
  I.IsPrime →
    (∃ (x : M), I = colon (M := M) ⊥ {x}) →
      ∀ (x : M) (h : I = colon (M := M) ⊥ {x}),
        ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
⊢ I.IsPrime →
    ((∃ (x : M), I = colon (M := M) ⊥ {x}) ↔
      ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M))
have refine_2 : I.IsPrime →
  (∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)) →
    ∀ (f : R ⧸ I →ₗ[R] M) (h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)),
      I = colon (M := M) ⊥ (singleton (α := M) ((f ∘ₗ mkQ I : (a : R) → M) 1 : M))
Tactic: refine fun _ ↦ ⟨fun ⟨x, h⟩ ↦ ?_, fun ⟨f, h⟩ ↦ ⟨(f ∘ₗ mkQ I) 1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
h_1 : I.IsPrime
h_2 : ∃ (x : M), I = colon (M := M) ⊥ {x}
x : M
h : I = colon (M := M) ⊥ {x}
⊢ ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
have h₁ : I = ker (toSpanSingleton R M x)
Tactic: replace h : I = ker (toSpanSingleton R M x) := by simp [h, SetLike.ext_iff]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
h_1 : I.IsPrime
h_2 : ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
f : R ⧸ I →ₗ[R] M
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
| I
have rw : (f ∘ₗ mkQ I).ker
Tactic: rw [← I.ker_mkQ, ← ker_comp_of_ker_eq_bot (mkQ I) (ker_eq_bot_of_injective h)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
h_1 : I.IsPrime
h_2 : ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
f : R ⧸ I →ₗ[R] M
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
⊢ I = colon (M := M) ⊥ (singleton (α := M) ((f ∘ₗ mkQ I : (a : R) → M) 1 : M))
have refine_2 : (f ∘ₗ mkQ I).ker = colon (M := M) ⊥ (singleton (α := M) ((f ∘ₗ mkQ I : (a : R) → M) 1 : M))
Tactic: conv_lhs => rw [← I.ker_mkQ, ← ker_comp_of_ker_eq_bot (mkQ I) (ker_eq_bot_of_injective h)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
h : IsAssociatedPrime J (R ⧸ I)
⊢ J = I.radical
have obtain : ∀ (hJ : J.IsPrime) (x : R ⧸ I) (e : J = Ideal.radical (colon (M := R ⧸ I) ⊥ {x})), J = I.radical
Tactic: obtain ⟨hJ, x, e⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
e : J = Ideal.radical (colon (M := R ⧸ I) ⊥ {0})
⊢ False
have apply : J = ⊤
Tactic: apply hJ.1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
e : J = Ideal.radical (colon (M := R ⧸ I) ⊥ {0})
⊢ J = ⊤
have rwa : ∀ (e : J = Ideal.radical ⊤), J = ⊤
Tactic: rwa [colon_singleton_zero, Ideal.radical_top] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
e : J = Ideal.radical (colon (M := R ⧸ I) ⊥ {0})
rwa : ∀ (e : J = Ideal.radical ⊤), J = ⊤
⊢ J = ⊤
have rwa₁ : ∀ (e : J = ⊤), J = ⊤
Tactic: rwa [colon_singleton_zero, Ideal.radical_top] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R ⧸ I
e : J = Ideal.radical (colon (M := R ⧸ I) ⊥ {x})
⊢ J = I.radical
have this : x ≠ 0
Tactic: have : x ≠ 0 := by
    rintro rfl
    apply hJ.1
    rwa [colon_singleton_zero, Ideal.radical_top] at e
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R ⧸ I
e : J = Ideal.radical (colon (M := R ⧸ I) ⊥ {x})
this : x ≠ 0
⊢ J = I.radical
have obtain : ∀ (x : R)
  (e :
    J =
      Ideal.radical
        (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I))))
  (this : Ne (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I)), J = I.radical
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mkₐ_surjective R _ x
Cleared hypotheses: x, e, this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : Ne (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I)
y : R
⊢ Membership.mem (γ := Ideal R)
      (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
have rw : Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
    (HSMul.hSMul (β := R ⧸ I) y ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
Tactic: rw [mem_colon_singleton, Algebra.smul_def, Ideal.Quotient.algebraMap_eq, ← map_mul, mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : Ne (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I)
y : R
rw :
  Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
      (HSMul.hSMul (β := R ⧸ I) y ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
⊢ Membership.mem (γ := Ideal R)
      (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
have rw₁ : Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
    (HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((algebraMap R (R ⧸ I) : (a : R) → R ⧸ I) y : R ⧸ I)
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
Tactic: rw [mem_colon_singleton, Algebra.smul_def, Ideal.Quotient.algebraMap_eq, ← map_mul, mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : Ne (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I)
y : R
rw :
  Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
      (HSMul.hSMul (β := R ⧸ I) y ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
rw₁ :
  Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
      (HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((algebraMap R (R ⧸ I) : (a : R) → R ⧸ I) y : R ⧸ I)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
⊢ Membership.mem (γ := Ideal R)
      (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
have rw₂ : Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
    (HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
Tactic: rw [mem_colon_singleton, Algebra.smul_def, Ideal.Quotient.algebraMap_eq, ← map_mul, mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : Ne (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I)
y : R
rw :
  Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
      (HSMul.hSMul (β := R ⧸ I) y ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
rw₁ :
  Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
      (HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((algebraMap R (R ⧸ I) : (a : R) → R ⧸ I) y : R ⧸ I)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
rw₂ :
  Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
      (HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
⊢ Membership.mem (γ := Ideal R)
      (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
have rw₃ : Membership.mem (α := R ⧸ I) (γ := Submodule R (R ⧸ I)) ⊥ ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) ↔
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
Tactic: rw [mem_colon_singleton, Algebra.smul_def, Ideal.Quotient.algebraMap_eq, ← map_mul, mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : Ne (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I)
y : R
rw :
  Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
      (HSMul.hSMul (β := R ⧸ I) y ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
rw₁ :
  Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
      (HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((algebraMap R (R ⧸ I) : (a : R) → R ⧸ I) y : R ⧸ I)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
rw₂ :
  Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
      (HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
rw₃ :
  Membership.mem (α := R ⧸ I) (γ := Submodule R (R ⧸ I)) ⊥ ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
⊢ Membership.mem (γ := Ideal R)
      (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
have rw₄ : Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I) ↔
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
Tactic: rw [mem_colon_singleton, Algebra.smul_def, Ideal.Quotient.algebraMap_eq, ← map_mul, mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : Ne (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I)
⊢ J = I.radical
have h : ∀ {y : R},
  Membership.mem (γ := Ideal R)
      (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
Tactic: have h {y} : y ∈ colon ⊥ {(Ideal.Quotient.mk I) x} ↔ Ideal.Quotient.mk I (y * x) = 0 := by
    rw [mem_colon_singleton, Algebra.smul_def, Ideal.Quotient.algebraMap_eq, ← map_mul, mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : Ne (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I)
h :
  ∀ {y : R},
    Membership.mem (γ := Ideal R)
        (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
⊢ J = I.radical
have simp : ∀ (this : x ∉ I)
  (h :
    ∀ {y : R},
      Membership.mem (γ := Ideal R)
          (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
        y * x ∈ I),
  Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) =
    I.radical
Tactic: simp only [e, Ideal.Quotient.mkₐ_eq_mk, ne_eq, Ideal.Quotient.eq_zero_iff_mem] at this h ⊢
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : x ∉ I
h :
  ∀ {y : R},
    Membership.mem (γ := Ideal R)
        (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
      y * x ∈ I
⊢ Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) =
    I.radical
have refine : ∀ (y : R)
  (hy :
    Membership.mem (γ := Submodule R R)
      (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y),
  y ∈ I.radical
Tactic: refine le_antisymm (Ideal.radical_le_radical_iff.mpr fun y hy ↦ ?_)
    (Ideal.radical_mono fun y ↦ h.mpr ∘ I.mul_mem_right x)