awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
refine_1 :
  Finset.inf
      (Finset.image (fun (t : Finset (Submodule R M)) ↦ t.inf id)
        (Finset.image (fun (J : Submodule R M) ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s))
      id =
    N
⊢ ∃ (t : Finset (Submodule R M)),
    t.inf id = N ∧
      (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
        (↑t : Set (Submodule R M)).Pairwise
          ((fun (x1 x2 : Ideal R) ↦ x1 ≠ x2) on fun (J : Submodule R M) ↦ (J.colon Set.univ).radical)
have refine_2 : ∀ ⦃J : Submodule R M⦄,
  Membership.mem (γ := Finset (Submodule R M))
      (Finset.image (fun (t : Finset (Submodule R M)) ↦ t.inf id)
        (Finset.image (fun (J : Submodule R M) ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s))
      J →
    J.IsPrimary
Tactic: classical
  refine ⟨(s.image fun J ↦ {I ∈ s | (I.colon .univ).radical = (J.colon .univ).radical}).image
    fun t ↦ t.inf id, ?_, ?_, ?_⟩
  · ext
    grind [Finset.inf_image, Submodule.mem_finsetInf]
  · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂]
    intro J hJ
    refine isPrimary_finsetInf (i := J) ?_ ?_ (by simp)
    · simp [hJ]
    · simp only [Finset.mem_filter, id_eq, and_imp]
      intro y hy
      simp [hs' hy]
  · intro I hI J hJ hIJ
    simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ
    obtain ⟨I', hI', hI⟩ := hI
    obtain ⟨J', hJ', hJ⟩ := hJ
    simp only [Function.onFun, ne_eq]
    contrapose hIJ
    suffices (I'.colon Set.univ).radical = (J'.colon Set.univ).radical by
      rw [← hI, ← hJ, this]
    · rw [← hI, colon_finsetInf,
        radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ
      rw [hIJ, ← hJ, colon_finsetInf,
        radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
refine_1 :
  Finset.inf
      (Finset.image (fun (t : Finset (Submodule R M)) ↦ t.inf id)
        (Finset.image (fun (J : Submodule R M) ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s))
      id =
    N
refine_2 :
  ∀ ⦃J : Submodule R M⦄,
    Membership.mem (γ := Finset (Submodule R M))
        (Finset.image (fun (t : Finset (Submodule R M)) ↦ t.inf id)
          (Finset.image (fun (J : Submodule R M) ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical})
            s))
        J →
      J.IsPrimary
⊢ ∃ (t : Finset (Submodule R M)),
    t.inf id = N ∧
      (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
        (↑t : Set (Submodule R M)).Pairwise
          ((fun (x1 x2 : Ideal R) ↦ x1 ≠ x2) on fun (J : Submodule R M) ↦ (J.colon Set.univ).radical)
have refine_3 : (↑(Finset.image (fun (t : Finset (Submodule R M)) ↦ t.inf id)
          (Finset.image (fun (J : Submodule R M) ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical})
            s)) :
      Set (Submodule R M)).Pairwise
  ((fun (x1 x2 : Ideal R) ↦ x1 ≠ x2) on fun (J : Submodule R M) ↦ (J.colon Set.univ).radical)
Tactic: classical
  refine ⟨(s.image fun J ↦ {I ∈ s | (I.colon .univ).radical = (J.colon .univ).radical}).image
    fun t ↦ t.inf id, ?_, ?_, ?_⟩
  · ext
    grind [Finset.inf_image, Submodule.mem_finsetInf]
  · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂]
    intro J hJ
    refine isPrimary_finsetInf (i := J) ?_ ?_ (by simp)
    · simp [hJ]
    · simp only [Finset.mem_filter, id_eq, and_imp]
      intro y hy
      simp [hs' hy]
  · intro I hI J hJ hIJ
    simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ
    obtain ⟨I', hI', hI⟩ := hI
    obtain ⟨J', hJ', hJ⟩ := hJ
    simp only [Function.onFun, ne_eq]
    contrapose hIJ
    suffices (I'.colon Set.univ).radical = (J'.colon Set.univ).radical by
      rw [← hI, ← hJ, this]
    · rw [← hI, colon_finsetInf,
        radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ
      rw [hIJ, ← hJ, colon_finsetInf,
        radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
⊢ ∃ (t : Finset (Submodule R M)),
    t.inf id = N ∧
      (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
        (↑t : Set (Submodule R M)).Pairwise
            ((fun (x1 x2 : Ideal R) ↦ x1 ≠ x2) on fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) ∧
          ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
have obtain : ∀ (t : Finset (Submodule R M)) (ht : t.inf id = N) (ht' : ∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary)
  (ht'' :
    (↑t : Set (Submodule R M)).Pairwise
      ((fun (x1 x2 : Ideal R) ↦ x1 ≠ x2) on fun (J : Submodule R M) ↦ (J.colon Set.univ).radical)),
  ∃ (t : Finset (Submodule R M)),
    t.inf id = N ∧
      (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
        (↑t : Set (Submodule R M)).Pairwise
            ((fun (x1 x2 : Ideal R) ↦ x1 ≠ x2) on fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) ∧
          ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
Tactic: obtain ⟨t, ht, ht', ht''⟩ := isPrimary_decomposition_pairwise_ne_radical hs hs'
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
t : Finset (Submodule R M)
ht : t.inf id = N
ht' : ∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary
ht'' :
  (↑t : Set (Submodule R M)).Pairwise
    ((fun (x1 x2 : Ideal R) ↦ x1 ≠ x2) on fun (J : Submodule R M) ↦ (J.colon Set.univ).radical)
⊢ ∃ (t : Finset (Submodule R M)),
    t.inf id = N ∧
      (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
        (↑t : Set (Submodule R M)).Pairwise
            ((fun (x1 x2 : Ideal R) ↦ x1 ≠ x2) on fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) ∧
          ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
have obtain : ∀ (u : Finset (Submodule R M)) (hut : u ⊆ t) (hu : u.inf id = N)
  (hu' : ∀ ⦃J : Submodule R M⦄, J ∈ u → ¬(u.erase J).inf id ≤ J),
  ∃ (t : Finset (Submodule R M)),
    t.inf id = N ∧
      (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
        (↑t : Set (Submodule R M)).Pairwise
            ((fun (x1 x2 : Ideal R) ↦ x1 ≠ x2) on fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) ∧
          ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
Tactic: obtain ⟨u, hut, hu, hu'⟩ := decomposition_erase_inf ht
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : IsLasker R M
N : Submodule R M
⊢ ∃ (t : Finset (Submodule R M)), N.IsMinimalPrimaryDecomposition t
have obtain : ∀ (s : Finset (Submodule R M)) (hs1 : s.inf id = N) (hs2 : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary),
  ∃ (t : Finset (Submodule R M)), N.IsMinimalPrimaryDecomposition t
Tactic: obtain ⟨s, hs1, hs2⟩ := h N
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : IsLasker R M
N : Submodule R M
s : Finset (Submodule R M)
hs1 : s.inf id = N
hs2 : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
⊢ ∃ (t : Finset (Submodule R M)), N.IsMinimalPrimaryDecomposition t
have obtain : ∀ (t : Finset (Submodule R M)) (h1 : t.inf id = N) (h2 : ∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary)
  (h3 :
    (↑t : Set (Submodule R M)).Pairwise
      ((fun (x1 x2 : Ideal R) ↦ x1 ≠ x2) on fun (J : Submodule R M) ↦ (J.colon Set.univ).radical))
  (h4 : ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J),
  ∃ (t : Finset (Submodule R M)), N.IsMinimalPrimaryDecomposition t
Tactic: obtain ⟨t, h1, h2, h3, h4⟩ :=
    exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition hs1 hs2
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
x : M
⊢ (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
have simp_rw : Eq.{u_1 + 1} (α := Ideal R) (t.inf fun (x_1 : Submodule R M) ↦ (x_1.colon {x}).radical)
  ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
Tactic: simp_rw [← ht.inf_eq, colon_finsetInf, ← radicalInfTopHom_apply, map_finset_inf,
      Function.comp_def, radicalInfTopHom_apply, id_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
x : M
⊢ Eq.{u_1 + 1} (α := Ideal R) (t.inf fun (x_1 : Submodule R M) ↦ (x_1.colon {x}).radical)
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
have rw : Eq.{u_1 + 1} (α := Ideal R) (t.inf fun (q : Submodule R M) ↦ if x ∈ q then ⊤ else (q.colon Set.univ).radical)
  ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
Tactic: rw [Finset.inf_congr rfl (fun q hq ↦ (ht.primary hq).radical_colon_singleton_eq_ite x),
      Finset.inf_ite, Finset.inf_top, top_inf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
x : M
rw :
  Eq.{u_1 + 1} (α := Ideal R) (t.inf fun (q : Submodule R M) ↦ if x ∈ q then ⊤ else (q.colon Set.univ).radical)
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
⊢ Eq.{u_1 + 1} (α := Ideal R) (t.inf fun (x_1 : Submodule R M) ↦ (x_1.colon {x}).radical)
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
have rw₁ : Eq.{u_1 + 1} (α := Ideal R)
  (({q ∈ t | x ∈ q}.inf fun (q : Submodule R M) ↦ ⊤) ⊓
    {i ∈ t | x ∉ i}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
  ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
Tactic: rw [Finset.inf_congr rfl (fun q hq ↦ (ht.primary hq).radical_colon_singleton_eq_ite x),
      Finset.inf_ite, Finset.inf_top, top_inf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
x : M
rw :
  Eq.{u_1 + 1} (α := Ideal R) (t.inf fun (q : Submodule R M) ↦ if x ∈ q then ⊤ else (q.colon Set.univ).radical)
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
rw₁ :
  Eq.{u_1 + 1} (α := Ideal R)
    (({q ∈ t | x ∈ q}.inf fun (q : Submodule R M) ↦ ⊤) ⊓
      {i ∈ t | x ∉ i}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
⊢ Eq.{u_1 + 1} (α := Ideal R) (t.inf fun (x_1 : Submodule R M) ↦ (x_1.colon {x}).radical)
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
have rw₂ : Eq.{u_1 + 1} (α := Ideal R) (⊤ ⊓ {i ∈ t | x ∉ i}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
  ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
Tactic: rw [Finset.inf_congr rfl (fun q hq ↦ (ht.primary hq).radical_colon_singleton_eq_ite x),
      Finset.inf_ite, Finset.inf_top, top_inf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
x : M
rw :
  Eq.{u_1 + 1} (α := Ideal R) (t.inf fun (q : Submodule R M) ↦ if x ∈ q then ⊤ else (q.colon Set.univ).radical)
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
rw₁ :
  Eq.{u_1 + 1} (α := Ideal R)
    (({q ∈ t | x ∈ q}.inf fun (q : Submodule R M) ↦ ⊤) ⊓
      {i ∈ t | x ∉ i}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
rw₂ :
  Eq.{u_1 + 1} (α := Ideal R) (⊤ ⊓ {i ∈ t | x ∉ i}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
⊢ Eq.{u_1 + 1} (α := Ideal R) (t.inf fun (x_1 : Submodule R M) ↦ (x_1.colon {x}).radical)
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
have rw₃ : Eq.{u_1 + 1} (α := Ideal R) ({i ∈ t | x ∉ i}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
  ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
Tactic: rw [Finset.inf_congr rfl (fun q hq ↦ (ht.primary hq).radical_colon_singleton_eq_ite x),
      Finset.inf_ite, Finset.inf_top, top_inf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)) = N.associatedPrimes
have h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
Tactic: replace h x : radical (N.colon {x}) = (t.filter (x ∉ ·)).inf fun q ↦ radical (q.colon .univ) := by
    simp_rw [← ht.inf_eq, colon_finsetInf, ← radicalInfTopHom_apply, map_finset_inf,
      Function.comp_def, radicalInfTopHom_apply, id_eq]
    rw [Finset.inf_congr rfl (fun q hq ↦ (ht.primary hq).radical_colon_singleton_eq_ite x),
      Finset.inf_ite, Finset.inf_top, top_inf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)) = N.associatedPrimes
have h₁ : ∀ (p : Ideal R),
  Membership.mem (γ := Set (Ideal R))
      ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) p ↔
    p ∈ N.associatedPrimes
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
p : Ideal R
⊢ Membership.mem (γ := Set (Ideal R))
      ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) p ↔
    p ∈ N.associatedPrimes
have h₁ : Membership.mem (γ := Set (Ideal R))
    ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) p →
  p ∈ N.associatedPrimes
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
p : Ideal R
h₁ :
  Membership.mem (γ := Set (Ideal R))
      ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) p →
    p ∈ N.associatedPrimes
⊢ Membership.mem (γ := Set (Ideal R))
      ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) p ↔
    p ∈ N.associatedPrimes
have h₂ : p ∈ N.associatedPrimes →
  Membership.mem (γ := Set (Ideal R))
    ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) p
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
q : Submodule R M
hqt : q ∈ (↑t : Set (Submodule R M))
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) q ∈ N.associatedPrimes
have h₁ : ∀ (x : M) (hxt : x ∈ (t.erase q).inf id) (hxq : x ∉ q),
  (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) q ∈ N.associatedPrimes
Tactic: obtain ⟨x, hxt, hxq⟩ := SetLike.not_le_iff_exists.mp (ht.minimal hqt)
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
q : Submodule R M
hqt : q ∈ (↑t : Set (Submodule R M))
x : M
hxt : x ∈ (t.erase q).inf id
hxq : x ∉ q
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) q ∈ N.associatedPrimes
have h₁ : (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) q = (N.colon {x}).radical
Tactic: use (ht.primary hqt).isPrime_radical_colon, x
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
q : Submodule R M
hqt : q ∈ (↑t : Set (Submodule R M))
x : M
hxt : x ∈ (t.erase q).inf id
hxq : x ∉ q
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) q = (N.colon {x}).radical
have h₁ : ∀ b ∈ {x_1 ∈ t | x ∉ x_1}.erase q, (q.colon Set.univ).radical ≤ (b.colon Set.univ).radical
Tactic: rw [h, ← Finset.insert_erase (Finset.mem_filter.mpr ⟨hqt, hxq⟩), Finset.inf_insert,
      eq_comm, inf_eq_left, Finset.le_inf_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
q : Submodule R M
hqt : q ∈ (↑t : Set (Submodule R M))
x : M
hxt : x ∈ (t.erase q).inf id
hxq : x ∉ q
⊢ ∀ b ∈ {x_1 ∈ t | x ∉ x_1}.erase q, (q.colon Set.univ).radical ≤ (b.colon Set.univ).radical
have hxt₁ : ∀ (i : Submodule R M), i ≠ q ∧ i ∈ t → x ∈ id i
Tactic: simp only [mem_finsetInf, Finset.mem_erase] at hxt
Cleared hypotheses: hxt
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
x : M
hp : (N.colon {x}).radical.IsPrime
⊢ Membership.mem (γ := Set (Ideal R))
    ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) (N.colon {x}).radical
have h₁ : ∀ (hp : IsPrime.{u_1} (α := R) ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)),
  Membership.mem (γ := Set (Ideal R))
    ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)))
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
Tactic: rw [h] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
x : M
hp : IsPrime.{u_1} (α := R) ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
⊢ Membership.mem (γ := Set (Ideal R))
    ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)))
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
have h₁ : ∀ (q : Submodule R M) (hq1 : q ∈ {x_1 ∈ t | x ∉ x_1})
  (hq2 : (q.colon Set.univ).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical),
  Membership.mem (γ := Set (Ideal R))
    ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)))
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
Tactic: obtain ⟨q, hq1, hq2⟩ := eq_inf_of_isPrime_inf hp
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)) = N.associatedPrimes
have replace : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
Tactic: classical
  replace h x : radical (N.colon {x}) = (t.filter (x ∉ ·)).inf fun q ↦ radical (q.colon .univ) := by
    simp_rw [← ht.inf_eq, colon_finsetInf, ← radicalInfTopHom_apply, map_finset_inf,
      Function.comp_def, radicalInfTopHom_apply, id_eq]
    rw [Finset.inf_congr rfl (fun q hq ↦ (ht.primary hq).radical_colon_singleton_eq_ite x),
      Finset.inf_ite, Finset.inf_top, top_inf_eq]
  ext p
  constructor
  · rintro ⟨q, hqt, rfl⟩
    obtain ⟨x, hxt, hxq⟩ := SetLike.not_le_iff_exists.mp (ht.minimal hqt)
    use (ht.primary hqt).isPrime_radical_colon, x
    rw [h, ← Finset.insert_erase (Finset.mem_filter.mpr ⟨hqt, hxq⟩), Finset.inf_insert,
      eq_comm, inf_eq_left, Finset.le_inf_iff]
    simp only [mem_finsetInf, Finset.mem_erase] at hxt
    grind
  · rintro ⟨hp, x, rfl⟩
    rw [h] at hp ⊢
    obtain ⟨q, hq1, hq2⟩ := eq_inf_of_isPrime_inf hp
    exact ⟨q, Finset.mem_of_mem_filter q hq1, hq2⟩