∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S) (I : Ideal R),
  I ≠ ⊤ →
    ∀ [inst_3 : Invertible x],
      Ideal.map (algebraMap R ↥R[x]) I ⊔ Ideal.span {⟨x, ⋯⟩} = ⊤ →
        ∃ p, p.leadingCoeff - 1 ∈ I ∧ (Polynomial.aeval ⅟x) p = 0