{𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {f : E → F} →
                  {p : FormalMultilinearSeries 𝕜 E F} →
                    {x : E} →
                      {n : ℕ} →
                        {r : ENNReal} →
                          {motive : HasFiniteFPowerSeriesOnBall f p x n r → Sort u} →
                            (t : HasFiniteFPowerSeriesOnBall f p x n r) →
                              ((toHasFPowerSeriesOnBall : HasFPowerSeriesOnBall f p x r) →
                                  (finite : ∀ (m : ℕ), n ≤ m → p m = 0) → motive ⋯) →
                                motive t