∀ {𝕜 : Type u_3} {E : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal}
  (motive : (∃ a ∈ Set.Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n) → Prop)
  (x : ∃ a ∈ Set.Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n),
  (∀ (w : ℝ) (ha : w ∈ Set.Ioo 0 1) (C : ℝ) (hC : C > 0) (h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * w ^ n), motive ⋯) →
    motive x