∀ {K : Type v} [inst : Field K] (f g : Polynomial K),
  IsCoprime f g ↔
    ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
      (Polynomial.aeval a) f ≠ 0 ∨ (Polynomial.aeval a) g ≠ 0