-- Mathlib/RingTheory/Lasker.lean
lemma isPrimary_decomposition_pairwise_ne_radical {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)

Proof state:
case refine_1.refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
x : R
hx : x ∈ s.inf id
⊢ x ∈
    (Finset.image (fun t => t.inf id) (Finset.image (fun J => Finset.filter (fun I => I.radical = J.radical) s) s)).inf
      id

Tactic:
simp only [Submodule.mem_finset_inf, id_eq, Finset.inf_image, CompTriple.comp_eq,
Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢

Result:
case refine_1.refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
x : R
hx : ∀ i ∈ s, x ∈ i
⊢ ∀ i ∈ s, ∀ i_1 ∈ s, i_1.radical = i.radical → x ∈ i_1

Proof state:
case refine_3.intro.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I✝ : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I✝
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
I J : Ideal R
hIJ : I ≠ J
I' : Ideal R
hI' : I' ∈ s
hI : (Finset.filter (fun I => I.radical = I'.radical) s).inf id = I
J' : Ideal R
hJ' : J' ∈ s
hJ : (Finset.filter (fun I => I.radical = J'.radical) s).inf id = J
⊢ ¬I.radical = J.radical

Tactic:
contrapose! hIJ

Result:
case refine_3.intro.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
I✝ : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I✝
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
I J I' : Ideal R
hI' : I' ∈ s
hI : (Finset.filter (fun I => I.radical = I'.radical) s).inf id = I
J' : Ideal R
hJ' : J' ∈ s
hJ : (Finset.filter (fun I => I.radical = J'.radical) s).inf id = J
hIJ : I.radical = J.radical
⊢ I = J

Proof state:
case refine_2.refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
J : Ideal R
hJ : J ∈ s
⊢ ∀ ⦃y : Ideal R⦄, y ∈ Finset.filter (fun I => I.radical = J.radical) s → (id y).IsPrimary

Tactic:
simp only [Finset.mem_filter, id_eq, and_imp]

Result:
case refine_2.refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
J : Ideal R
hJ : J ∈ s
⊢ ∀ ⦃y : Ideal R⦄, y ∈ s → y.radical = J.radical → y.IsPrimary

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I✝ : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I✝
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
I J I' : Ideal R
hI' : I' ∈ s
hI : (Finset.filter (fun I => I.radical = I'.radical) s).inf id = I
J' : Ideal R
hJ' : J' ∈ s
hJ : (Finset.filter (fun I => I.radical = J'.radical) s).inf id = J
hIJ : I.radical = J.radical
this : I'.radical = J'.radical
⊢ I = J

Tactic:
rw [← hI, ← hJ, this]

Result:
no goals

Proof state:
case refine_2.refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
J : Ideal R
hJ : J ∈ s
⊢ ∀ ⦃y : Ideal R⦄, y ∈ s → y.radical = J.radical → y.IsPrimary

Tactic:
intro y hy

Result:
case refine_2.refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
J : Ideal R
hJ : J ∈ s
y : Ideal R
hy : y ∈ s
⊢ y.radical = J.radical → y.IsPrimary

Proof state:
R : Type u_1
inst✝ : CommSemiring 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)

Tactic:
refine ⟨(s.image (fun J ↦ s.filter (fun I ↦ I.radical = J.radical))).image fun t ↦ t.inf id,
  ?_, ?_, ?_⟩

Result:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
⊢ (Finset.image (fun t => t.inf id) (Finset.image (fun J => Finset.filter (fun I => I.radical = J.radical) s) s)).inf
      id =
    I

case refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
⊢ ∀ ⦃J : Ideal R⦄,
    J ∈ Finset.image (fun t => t.inf id) (Finset.image (fun J => Finset.filter (fun I => I.radical = J.radical) s) s) →
      J.IsPrimary

case refine_3
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
⊢ (↑(Finset.image (fun t => t.inf id)
          (Finset.image (fun J => Finset.filter (fun I => I.radical = J.radical) s) s))).Pairwise
    ((fun x1 x2 => x1 ≠ x2) on radical)

Proof state:
case refine_3
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
⊢ (↑(Finset.image (fun t => t.inf id)
          (Finset.image (fun J => Finset.filter (fun I => I.radical = J.radical) s) s))).Pairwise
    ((fun x1 x2 => x1 ≠ x2) on radical)

Tactic:
intro I hI J hJ hIJ

Result:
case refine_3
R : Type u_1
inst✝ : CommSemiring R
I✝ : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I✝
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
I : Ideal R
hI :
  I ∈ ↑(Finset.image (fun t => t.inf id) (Finset.image (fun J => Finset.filter (fun I => I.radical = J.radical) s) s))
J : Ideal R
hJ :
  J ∈ ↑(Finset.image (fun t => t.inf id) (Finset.image (fun J => Finset.filter (fun I => I.radical = J.radical) s) s))
hIJ : I ≠ J
⊢ ((fun x1 x2 => x1 ≠ x2) on radical) I J

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I✝ : Ideal R
s : Finset (Ideal R)
hs : s.inf id = I✝
hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary
I J I' : Ideal R
hI' : I' ∈ s
hI : (Finset.filter (fun I => I.radical = I'.radical) s).inf id = I
J' : Ideal R
hJ' : J' ∈ s
hJ : (Finset.filter (fun I => I.radical = J'.radical) s).inf id = J
hIJ : ((Finset.filter (fun I => I.radical = I'.radical) s).inf id).radical = J.radical
⊢ ∀ ⦃y : Ideal R⦄, y ∈ Finset.filter (fun I => I.radical = I'.radical) s → (id y).radical = (id I').radical

Tactic:
simp

Result:
no goals