rw [hf i (Finset.mem_insert_self i s), mul_one]
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ I + K = I + K * (I + J i)
no goals