∀ {ι : Type u_1} {R : Type u_2} {S : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (S i)]
  [inst_2 : (i : ι) → Algebra R (S i)] {s : Set ι} {t : (i : ι) → Subalgebra R (S i)} {x : (i : ι) → S i},
  (x ∈ Subalgebra.pi s t) = ∀ i ∈ s, x i ∈ t i