∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] {s : Set ι} {i : ι},
  i ∉ s →
    (AlgebraicIndepOn R x (insert i s) ↔ AlgebraicIndepOn R x s ∧ Transcendental (↥(Algebra.adjoin R (x '' s))) (x i))