-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι} (hp : ∀ i ∈ s, (f i).IsPrime) (hn : s.card = n)
    (h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)),
    I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
s : Finset ι
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
hn : s.card = n + 1
h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
succ succ₁ succ₂ :
  ∀ (hn : ∃ (i : ι) (t : Finset ι), i ∉ t ∧ insert i t = s ∧ t.card = n), I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
succ₃ :
  ∀ (i : ι) (t : Finset ι) (hit : i ∉ t) (hn : t.card = n) (hp : ∀ i_1 ∈ insert i t, (f i_1).IsPrime)
    (h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R)),
    I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
succ₄ :
  ∀ (i : ι) (t : Finset ι) (hit : i ∉ t) (hn : t.card = n)
    (h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R))
    (hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime), I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
pos :
  ∀ (i : ι) (t : Finset ι) (hit : i ∉ t) (hn : t.card = n)
    (h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R))
    (hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime) (Ht : ∃ j ∈ t, f j ≤ f i),
    I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
neg neg₁ :
  ∀ (i : ι) (t : Finset ι) (hit : i ∉ t) (hn : t.card = n)
    (h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R))
    (hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime) (Ht : ¬∃ j ∈ t, f j ≤ f i),
    I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
have pos₁ : ∀ (i : ι) (t : Finset ι) (hit : i ∉ t) (hn : t.card = n)
  (h : (↑I : Set R) ⊆ (↑(f a) : Set R) ∪ (↑(f b) : Set R) ∪ ⋃ i_1 ∈ (↑(insert i t) : Set ι), (↑(f i_1) : Set R))
  (hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime) (Ht : ¬∃ j ∈ t, f j ≤ f i) (Ha : f a ≤ f i),
  I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Tactic: classical
    replace hn : ∃ (i : ι) (t : Finset ι), i ∉ t ∧ insert i t = s ∧ t.card = n :=
      Finset.card_eq_succ.1 hn
    rcases hn with ⟨i, t, hit, rfl, hn⟩
    replace hp : IsPrime (f i) ∧ ∀ x ∈ t, IsPrime (f x) := (t.forall_mem_insert _ _).1 hp
    by_cases Ht : ∃ j ∈ t, f j ≤ f i
    · obtain ⟨j, hjt, hfji⟩ : ∃ j ∈ t, f j ≤ f i := Ht
      obtain ⟨u, hju, rfl⟩ : ∃ u, j ∉ u ∧ insert j u = t :=
        ⟨t.erase j, t.notMem_erase j, Finset.insert_erase hjt⟩
      have hp' : ∀ k ∈ insert i u, IsPrime (f k) := by
        rw [Finset.forall_mem_insert] at hp ⊢
        exact ⟨hp.1, hp.2.2⟩
      have hiu : i ∉ u := mt Finset.mem_insert_of_mem hit
      have hn' : (insert i u).card = n := by
        rwa [Finset.card_insert_of_notMem] at hn ⊢
        exacts [hiu, hju]
      have h' : (I : Set R) ⊆ f a ∪ f b ∪ ⋃ k ∈ (↑(insert i u) : Set ι), f k := by
        rw [Finset.coe_insert] at h ⊢
        rw [Finset.coe_insert] at h
        simp only [Set.biUnion_insert] at h ⊢
        rw [← Set.union_assoc (f i : Set R),
            Set.union_eq_self_of_subset_right hfji] at h
        exact h
      specialize ih hp' hn' h'
      refine ih.imp id (Or.imp id (Exists.imp fun k => ?_))
      exact And.imp (fun hk => Finset.insert_subset_insert i (Finset.subset_insert j u) hk) id
    by_cases Ha : f a ≤ f i
    · have h' : (I : Set R) ⊆ f i ∪ f b ∪ ⋃ j ∈ (↑t : Set ι), f j := by
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_assoc,
          Set.union_right_comm (f a : Set R),
          Set.union_eq_self_of_subset_left Ha] at h
        exact h
      specialize ih hp.2 hn h'
      right
      rcases ih with (ih | ih | ⟨k, hkt, ih⟩)
      · exact Or.inr ⟨i, Finset.mem_insert_self i t, ih⟩
      · exact Or.inl ih
      · exact Or.inr ⟨k, Finset.mem_insert_of_mem hkt, ih⟩
    by_cases Hb : f b ≤ f i
    · have h' : (I : Set R) ⊆ f a ∪ f i ∪ ⋃ j ∈ (↑t : Set ι), f j := by
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_assoc,
          Set.union_assoc (f a : Set R),
          Set.union_eq_self_of_subset_left Hb] at h
        exact h
      specialize ih hp.2 hn h'
      rcases ih with (ih | ih | ⟨k, hkt, ih⟩)
      · exact Or.inl ih
      · exact Or.inr (Or.inr ⟨i, Finset.mem_insert_self i t, ih⟩)
      · exact Or.inr (Or.inr ⟨k, Finset.mem_insert_of_mem hkt, ih⟩)
    by_cases Hi : I ≤ f i
    · exact Or.inr (Or.inr ⟨i, Finset.mem_insert_self i t, Hi⟩)
    have : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i := by
      simp only [hp.1.inf_le, hp.1.inf_le', not_or]
      exact ⟨⟨⟨Hi, Ha⟩, Hb⟩, Ht⟩
    rcases Set.not_subset.1 this with ⟨r, ⟨⟨⟨hrI, hra⟩, hrb⟩, hr⟩, hri⟩
    by_cases HI : (I : Set R) ⊆ f a ∪ f b ∪ ⋃ j ∈ (↑t : Set ι), f j
    · specialize ih hp.2 hn HI
      rcases ih with (ih | ih | ⟨k, hkt, ih⟩)
      · order
      · order
      · right
        right
        exact ⟨k, Finset.mem_insert_of_mem hkt, ih⟩
    exfalso
    rcases Set.not_subset.1 HI with ⟨s, hsI, hs⟩
    rw [Finset.coe_insert, Set.biUnion_insert] at h
    have hsi : s ∈ f i := ((h hsI).resolve_left (mt Or.inl hs)).resolve_right (mt Or.inr hs)
    rcases h (I.add_mem hrI hsI) with (⟨ha | hb⟩ | hi | ht)
    · exact hs (Or.inl <| Or.inl <| add_sub_cancel_left r s ▸ (f a).sub_mem ha hra)
    · exact hs (Or.inl <| Or.inr <| add_sub_cancel_left r s ▸ (f b).sub_mem hb hrb)
    · exact hri (add_sub_cancel_right r s ▸ (f i).sub_mem hi hsi)
    · rw [Set.mem_iUnion₂] at ht
      rcases ht with ⟨j, hjt, hj⟩
      simp only [Finset.inf_eq_iInf, SetLike.mem_coe, Submodule.mem_iInf] at hr
      exact hs <| Or.inr <| Set.mem_biUnion hjt <|
        add_sub_cancel_left r s ▸ (f j).sub_mem hj <| hr j hjt
Cleared hypotheses: s, hp, hn, h