awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Lasker
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
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I.colon Set.univ).radical = (J.colon Set.univ).radical
refine_3 : (I'.colon Set.univ).radical = (J'.colon Set.univ).radical
⊢ I = J

Tactic:
suffices (I'.colon Set.univ).radical = (J'.colon Set.univ).radical by
      rw [← hI, ← hJ, this]
-- Module: Mathlib.RingTheory.Lasker
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
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ :
  radical
      ({I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf fun (i : Submodule R M) ↦
        (id i).colon Set.univ) =
    (J.colon Set.univ).radical
⊢ I' ∈ {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}

Tactic:
simp [hI']
-- Module: Mathlib.RingTheory.Lasker
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
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ :
  radical
      ({I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf fun (i : Submodule R M) ↦
        (id i).colon Set.univ) =
    (J.colon Set.univ).radical
⊢ ∀ ⦃y : Submodule R M⦄,
    y ∈ {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical} →
      ((id y).colon Set.univ).radical = ((id I').colon Set.univ).radical

Tactic:
simp
-- Module: Mathlib.RingTheory.Lasker
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
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I.colon Set.univ).radical = (J.colon Set.univ).radical
⊢ (I'.colon Set.univ).radical = (J.colon Set.univ).radical

Tactic:
rw [← hI, colon_finsetInf,
        radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ

Premises used: Submodule.colon_finsetInf, Ideal.radical_finset_inf, id_eq
-- Module: Mathlib.RingTheory.Lasker
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
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I'.colon Set.univ).radical = (J.colon Set.univ).radical
⊢ J' ∈ {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}

Tactic:
simp [hJ']
-- Module: Mathlib.RingTheory.Lasker
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
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I'.colon Set.univ).radical = (J.colon Set.univ).radical
⊢ ∀ ⦃y : Submodule R M⦄,
    y ∈ {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical} →
      ((id y).colon Set.univ).radical = ((id J').colon Set.univ).radical

Tactic:
simp
-- Module: Mathlib.RingTheory.Lasker
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
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I'.colon Set.univ).radical = (J.colon Set.univ).radical
refine_3 : (J.colon Set.univ).radical = (J'.colon Set.univ).radical
refine_3₁ :
  (({I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id).colon Set.univ).radical =
    (J'.colon Set.univ).radical
refine_3₂ :
  radical
      ({I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf fun (i : Submodule R M) ↦
        (id i).colon Set.univ) =
    (J'.colon Set.univ).radical
refine_3₃ : ((id J').colon Set.univ).radical = (J'.colon Set.univ).radical
refine_3₄ refine_3₅ : (J'.colon Set.univ).radical = (J'.colon Set.univ).radical
⊢ (I'.colon Set.univ).radical = (J'.colon Set.univ).radical

Tactic:
rw [hIJ, ← hJ, colon_finsetInf,
        radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq]

Premises used: Submodule.colon_finsetInf, Ideal.radical_finset_inf, id_eq
-- Module: Mathlib.RingTheory.Lasker
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
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
⊢ ∃ (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'

Premises used: Submodule.isPrimary_decomposition_pairwise_ne_radical
-- Module: Mathlib.RingTheory.Lasker
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)
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
⊢ ∃ (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

Premises used: Submodule.decomposition_erase_inf
-- Module: Mathlib.RingTheory.Lasker
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)
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:
⟨u, hu, fun _ hi ↦ ht' (hut hi), ht''.mono hut, hu'⟩

Premises used: Set.Pairwise.mono, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Lasker
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)
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:
exact ⟨u, hu, fun _ hi ↦ ht' (hut hi), ht''.mono hut, hu'⟩
-- Module: Mathlib.RingTheory.Lasker
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
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
⊢ ∃ (t : Finset (Submodule R M)), N.IsMinimalPrimaryDecomposition t

Tactic:
obtain ⟨s, hs1, hs2⟩ := h N
-- Module: Mathlib.RingTheory.Lasker
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
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
⊢ ∃ (t : Finset (Submodule R M)), N.IsMinimalPrimaryDecomposition t

Tactic:
obtain ⟨t, h1, h2, h3, h4⟩ :=
    exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition hs1 hs2

Premises used: Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition
-- Module: Mathlib.RingTheory.Lasker
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)
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:
⟨t, h1, h2, h3, h4⟩

Premises used: Submodule.IsMinimalPrimaryDecomposition.mk, Exists.intro
-- Module: Mathlib.RingTheory.Lasker
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)
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:
exact ⟨t, h1, h2, h3, h4⟩
-- Module: Mathlib.RingTheory.Lasker
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
⊢ Set.InjOn.{u_2, u_1} (β := Ideal R) (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) (↑t : Set (Submodule R M))

Tactic:
Set.injOn_iff_pairwise_ne.mpr ht.distinct

Premises used: Iff.mpr, Submodule.IsMinimalPrimaryDecomposition.distinct, Set.injOn_iff_pairwise_ne
-- Module: Mathlib.RingTheory.Lasker
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
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)
⊢ (N.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]

Premises used: Submodule.colon_finsetInf, Submodule.IsMinimalPrimaryDecomposition.inf_eq, map_finset_inf, Function.comp_def, Ideal.radicalInfTopHom_apply, id_eq
-- Module: Mathlib.RingTheory.Lasker
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)
rw₃ 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)

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]

Premises used: Finset.inf_ite, Finset.inf_congr, top_inf_eq, Submodule.IsPrimary.radical_colon_singleton_eq_ite, Submodule.IsMinimalPrimaryDecomposition.primary, Finset.inf_top, rfl
-- Module: Mathlib.RingTheory.Lasker
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

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]
-- Module: Mathlib.RingTheory.Lasker
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
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
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)) = N.associatedPrimes

Tactic:
ext p
-- Module: Mathlib.RingTheory.Lasker
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
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
⊢ 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
-- Module: Mathlib.RingTheory.Lasker
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))
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
⊢ (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)

Premises used: Submodule.IsMinimalPrimaryDecomposition.minimal, Iff.mp, SetLike.not_le_iff_exists
-- Module: Mathlib.RingTheory.Lasker
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
h₁ : (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) q = (N.colon {x}).radical
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) q ∈ N.associatedPrimes

Tactic:
use (ht.primary hqt).isPrime_radical_colon, x

Premises used: Submodule.IsPrimary.isPrime_radical_colon, Submodule.IsMinimalPrimaryDecomposition.primary
-- Module: Mathlib.RingTheory.Lasker
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
h₁ : ∀ b ∈ {x_1 ∈ t | x ∉ x_1}.erase q, (q.colon Set.univ).radical ≤ (b.colon Set.univ).radical
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) q = (N.colon {x}).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]

Premises used: Iff.mpr, eq_comm, Finset.inf_insert, Finset.le_inf_iff, And.intro, inf_eq_left, Finset.mem_filter, Finset.insert_erase
-- Module: Mathlib.RingTheory.Lasker
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
⊢ ∀ (i : Submodule R M), i ≠ q ∧ i ∈ t → x ∈ id i

Tactic:
simp only [mem_finsetInf, Finset.mem_erase] at hxt

Premises used: Finset.mem_erase, Submodule.mem_finsetInf
-- Module: Mathlib.RingTheory.Lasker
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
hxq : x ∉ q
hxt : ∀ (i : Submodule R M), i ≠ q ∧ i ∈ t → x ∈ id i
⊢ ∀ b ∈ {x_1 ∈ t | x ∉ x_1}.erase q, (q.colon Set.univ).radical ≤ (b.colon Set.univ).radical

Tactic:
grind
-- Module: Mathlib.RingTheory.Lasker
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
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)
⊢ Membership.mem (γ := Set (Ideal R))
    ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) (N.colon {x}).radical

Tactic:
rw [h] at hp ⊢
-- Module: Mathlib.RingTheory.Lasker
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)
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)
⊢ 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

Premises used: Ideal.eq_inf_of_isPrime_inf