∀ {R : Type u_2} [inst : CommSemiring R] {ι : Type u_1} {I : ι → Ideal R} {x : ι → R} (a : ι) (s_1 : Finset ι),
  a ∉ s_1 →
    ((∀ i ∈ s_1, x i ∈ I i) → ∏ i ∈ s_1, x i ∈ ∏ i ∈ s_1, I i) →
      (∀ i ∈ insert a s_1, x i ∈ I i) → ∏ i ∈ insert a s_1, x i ∈ ∏ i ∈ insert a s_1, I i