-- Mathlib/RingTheory/Lasker.lean
lemma exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition [DecidableEq (Ideal R)]
    {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) :
    ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧
      ((t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical)) ∧
      (∀ ⦃J⦄, J ∈ t → ¬ (t.erase J).inf id ≤ J)

Proof state:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
t : Finset (Ideal R)
ht : t.inf id = I
ht' : ∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary
ht'' : (↑t).Pairwise ((fun x1 x2 => x1 ≠ x2) on radical)
⊢ ∃ t,
    t.inf id = I ∧
      (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧
        (↑t).Pairwise ((fun x1 x2 => x1 ≠ x2) on radical) ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
obtain ⟨u, hut, hu, hu'⟩ := decomposition_erase_inf ht

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
t : Finset (Ideal R)
ht : t.inf id = I
ht' : ∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary
ht'' : (↑t).Pairwise ((fun x1 x2 => x1 ≠ x2) on radical)
u : Finset (Ideal R)
hut : u ⊆ t
hu : u.inf id = I
hu' : ∀ ⦃J : Ideal R⦄, J ∈ u → ¬(u.erase J).inf id ≤ J
⊢ ∃ t,
    t.inf id = I ∧
      (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧
        (↑t).Pairwise ((fun x1 x2 => x1 ≠ x2) on radical) ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
t : Finset (Ideal R)
ht : t.inf id = I
ht' : ∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary
ht'' : (↑t).Pairwise ((fun x1 x2 => x1 ≠ x2) on radical)
u : Finset (Ideal R)
hut : u ⊆ t
hu : u.inf id = I
hu' : ∀ ⦃J : Ideal R⦄, J ∈ u → ¬(u.erase J).inf id ≤ J
⊢ ∃ t,
    t.inf id = I ∧
      (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧
        (↑t).Pairwise ((fun x1 x2 => x1 ≠ x2) on radical) ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
exact ⟨u, hu, fun _ hi ↦ ht' (hut hi), ht''.mono hut, hu'⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
⊢ ∃ t,
    t.inf id = I ∧
      (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧
        (↑t).Pairwise ((fun x1 x2 => x1 ≠ x2) on radical) ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
obtain ⟨t, ht, ht', ht''⟩ := isPrimary_decomposition_pairwise_ne_radical hs hs'

Result:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
t : Finset (Ideal R)
ht : t.inf id = I
ht' : ∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary
ht'' : (↑t).Pairwise ((fun x1 x2 => x1 ≠ x2) on radical)
⊢ ∃ t,
    t.inf id = I ∧
      (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧
        (↑t).Pairwise ((fun x1 x2 => x1 ≠ x2) on radical) ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J