induction s using Finset.induction with
| empty =>
    simp
| @insert i s _ hs =>
    intro h
    rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
    set K := ⨅ j ∈ s, J j
    calc
      1 = I + K            := (hs fun j hj ↦ h j (Finset.mem_insert_of_mem hj)).symm
      _ = I + K*(I + J i)  := by rw [h i (Finset.mem_insert_self i s), mul_one]
      _ = (1+K)*I + K*J i  := by ring
      _ ≤ I + K ⊓ J i      := add_le_add mul_le_left mul_le_inf
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
s : Finset ι
⊢ (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
no goals