rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
h : ∀ j ∈ insert i s, I + J j = 1
⊢ I + ⨅ (j : ι) (_ : j ∈ insert i s), J j = 1
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
h : ∀ j ∈ insert i s, I + J j = 1
⊢ 1 ≤ I + (⨅ (x : ι) (_ : x ∈ s), J x) ⊓ J i