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
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ (j : ι) (_ : j ∈ s), J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ 1 ≤ I + K ⊓ J i
no goals