-- Mathlib/RingTheory/Lasker.lean
lemma decomposition_erase_inf [DecidableEq (Ideal R)] {I : Ideal R}
    {s : Finset (Ideal R)} (hs : s.inf id = I) :
    ∃ t : Finset (Ideal R), t ⊆ s ∧ t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → ¬ (t.erase J).inf id ≤ J)

Proof state:
case neg.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
J : Ideal R
hs : (insert J (s.erase J)).inf id = I
hJ : J ∈ s
hJ' : (s.erase J).inf id ≤ J
⊢ (s.erase J).inf id = I

Tactic:
simp [← hs, hJ']

Result:
no goals

Proof state:
case neg.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s.inf id = I
J : Ideal R
hJ : J ∈ s
hJ' : (s.erase J).inf id ≤ J
⊢ (s.erase J).inf id = I

Tactic:
rw [← Finset.insert_erase hJ] at hs

Result:
case neg.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
J : Ideal R
hs : (insert J (s.erase J)).inf id = I
hJ : J ∈ s
hJ' : (s.erase J).inf id ≤ J
⊢ (s.erase J).inf id = I

Proof state:
case a
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s.inf id = I
⊢ ∃ t ⊆ s, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
by_cases H : ∀ J ∈ s, ¬ (s.erase J).inf id ≤ J

Result:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s.inf id = I
H : ∀ J ∈ s, ¬(s.erase J).inf id ≤ J
⊢ ∃ t ⊆ s, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

case neg
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s.inf id = I
H : ¬∀ J ∈ s, ¬(s.erase J).inf id ≤ J
⊢ ∃ t ⊆ s, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Proof state:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s.inf id = I
H : ∀ J ∈ s, ¬(s.erase J).inf id ≤ J
⊢ ∃ t ⊆ s, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
exact ⟨s, Finset.Subset.rfl, hs, H⟩

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s✝ : Finset (Ideal R)
a✝ : ∀ t ⊂ s✝, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s✝.inf id = I
⊢ ∃ t ⊆ s✝, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
rename_i _ s IH

Result:
case a
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s.inf id = I
⊢ ∃ t ⊆ s, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

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
⊢ ∃ t ⊆ s, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
induction s using Finset.strongInductionOn

Result:
case a
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s✝ : Finset (Ideal R)
a✝ : ∀ t ⊂ s✝, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s✝.inf id = I
⊢ ∃ t ⊆ s✝, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Proof state:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s.inf id = I
H : ∃ J ∈ s, (s.erase J).inf id ≤ J
⊢ ∃ t ⊆ s, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

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

Result:
case neg.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s.inf id = I
J : Ideal R
hJ : J ∈ s
hJ' : (s.erase J).inf id ≤ J
⊢ ∃ t ⊆ s, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Proof state:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s.inf id = I
H : ¬∀ J ∈ s, ¬(s.erase J).inf id ≤ J
⊢ ∃ t ⊆ s, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
push_neg at H

Result:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s.inf id = I
H : ∃ J ∈ s, (s.erase J).inf id ≤ J
⊢ ∃ t ⊆ s, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Proof state:
case neg.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s.inf id = I
J : Ideal R
hJ : J ∈ s
hJ' : (s.erase J).inf id ≤ J
⊢ ∃ t ⊆ s, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
refine (IH (s.erase J) (Finset.erase_ssubset hJ) ?_).imp
  fun t ↦ And.imp_left (fun ht ↦ ht.trans (Finset.erase_subset _ _))

Result:
case neg.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
s : Finset (Ideal R)
IH : ∀ t ⊂ s, t.inf id = I → ∃ t_1 ⊆ t, t_1.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t_1 → ¬(t_1.erase J).inf id ≤ J
hs : s.inf id = I
J : Ideal R
hJ : J ∈ s
hJ' : (s.erase J).inf id ≤ J
⊢ (s.erase J).inf id = I