simp_rw [isCoprime_iff_add] at *
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, IsCoprime I (J j)
⊢ IsCoprime I (⨅ j ∈ s, J j)
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, I + J j = 1
⊢ I + ⨅ j ∈ s, J j = 1