-- 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
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

Tactic:
rw [← hs]

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 =
    s.inf id

Proof state:
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
hJ : J ∈ s
⊢ ((Finset.filter (fun I => I.radical = J.radical) s).inf id).IsPrimary

Tactic:
refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp)

Result:
case refine_2.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
J : Ideal R
hJ : J ∈ s
⊢ J ∈ Finset.filter (fun I => I.radical = J.radical) s

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

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 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'.radical = J'.radical

Tactic:
rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at 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'.radical = J'.radical

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 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

Tactic:
suffices I'.radical = J'.radical by
  rw [← hI, ← hJ, this]

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'.radical = J'.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 : ∀ i ∈ s, x ∈ i
⊢ ∀ i ∈ s, ∀ i_1 ∈ s, i_1.radical = i.radical → x ∈ i_1

Tactic:
intro J _ K hK _

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
J : Ideal R
a✝¹ : J ∈ s
K : Ideal R
hK : K ∈ s
a✝ : K.radical = J.radical
⊢ x ∈ K

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 : ∀ i ∈ s, x ∈ i
J : Ideal R
a✝¹ : J ∈ s
K : Ideal R
hK : K ∈ s
a✝ : K.radical = J.radical
⊢ x ∈ K

Tactic:
exact hx K hK

Result:
no goals

Proof state:
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

Tactic:
simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp,
forall_apply_eq_imp_iff₂]

Result:
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
⊢ ∀ a ∈ s, ((Finset.filter (fun I => I.radical = a.radical) s).inf id).IsPrimary

Proof state:
case refine_1.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
x : R
hx : ∀ i ∈ s, ∀ i_1 ∈ s, i_1.radical = i.radical → x ∈ i_1
⊢ ∀ i ∈ s, x ∈ i

Tactic:
intro J hJ

Result:
case refine_1.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
x : R
hx : ∀ i ∈ s, ∀ i_1 ∈ s, i_1.radical = i.radical → x ∈ i_1
J : Ideal R
hJ : J ∈ s
⊢ x ∈ J

Proof state:
case refine_1.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
x : R
hx : ∀ i ∈ s, ∀ i_1 ∈ s, i_1.radical = i.radical → x ∈ i_1
J : Ideal R
hJ : J ∈ s
⊢ x ∈ J

Tactic:
exact hx J hJ J hJ rfl

Result:
no goals

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 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'.radical = J'.radical

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

Result:
no goals

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
⊢ ((fun x1 x2 => x1 ≠ x2) on radical) I J

Tactic:
simp only [Function.onFun, ne_eq]

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 : 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