{R : Type u} →
  [inst : CommSemiring R] →
    {f : Polynomial R} →
      {𝓟 : Ideal R} →
        {motive : f.IsWeaklyEisensteinAt 𝓟 → Sort u_1} →
          (t : f.IsWeaklyEisensteinAt 𝓟) → ((mem : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟) → motive ⋯) → motive t