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

Tactic:
simp [hJ]

Result:
no goals

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
J : Ideal R
hJ : J ∈ s
⊢ ∀ ⦃y : Ideal R⦄, y ∈ Finset.filter (fun I => I.radical = J.radical) s → (id y).radical = (id J).radical

Tactic:
simp

Result:
no goals

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
⊢ ∀ ⦃y : Ideal R⦄, y ∈ Finset.filter (fun I => I.radical = J'.radical) s → (id y).radical = (id J').radical

Tactic:
simp

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

Tactic:
intro J hJ

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

Tactic:
simp [hJ']

Result:
no goals

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

Tactic:
refine le_antisymm ?_ ?_ <;> intro x hx

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 :
  x ∈
    (Finset.image (fun t => t.inf id) (Finset.image (fun J => Finset.filter (fun I => I.radical = J.radical) s) s)).inf
      id
⊢ x ∈ s.inf id

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

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
⊢ I' ∈ Finset.filter (fun I => I.radical = I'.radical) s

Tactic:
simp [hI']

Result:
no goals

Proof state:
case refine_3.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
hJ : ∃ a ∈ s, (Finset.filter (fun I => I.radical = a.radical) s).inf id = J
I' : Ideal R
hI' : I' ∈ s
hI : (Finset.filter (fun I => I.radical = I'.radical) s).inf id = I
⊢ ((fun x1 x2 => x1 ≠ x2) on radical) I J

Tactic:
obtain ⟨J', hJ', hJ⟩ := hJ

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

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
I J : Ideal R
hIJ : I ≠ J
hI : ∃ a ∈ s, (Finset.filter (fun I => I.radical = a.radical) s).inf id = I
hJ : ∃ a ∈ s, (Finset.filter (fun I => I.radical = a.radical) s).inf id = J
⊢ ((fun x1 x2 => x1 ≠ x2) on radical) I J

Tactic:
obtain ⟨I', hI', hI⟩ := hI

Result:
case refine_3.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
hJ : ∃ a ∈ s, (Finset.filter (fun I => I.radical = a.radical) s).inf id = J
I' : Ideal R
hI' : I' ∈ s
hI : (Finset.filter (fun I => I.radical = I'.radical) s).inf id = I
⊢ ((fun x1 x2 => x1 ≠ x2) on radical) I J

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

Tactic:
simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ

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 J : Ideal R
hIJ : I ≠ J
hI : ∃ a ∈ s, (Finset.filter (fun I => I.radical = a.radical) s).inf id = I
hJ : ∃ a ∈ s, (Finset.filter (fun I => I.radical = a.radical) s).inf id = J
⊢ ((fun x1 x2 => x1 ≠ x2) on 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
hy : y ∈ s
⊢ y.radical = J.radical → y.IsPrimary

Tactic:
simp [hs' hy]

Result:
no goals

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 :
  x ∈
    (Finset.image (fun t => t.inf id) (Finset.image (fun J => Finset.filter (fun I => I.radical = J.radical) s) s)).inf
      id
⊢ x ∈ s.inf id

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

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
⊢ ∀ i ∈ s, x ∈ i