{ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] →
                    {s : Set M} →
                      FunLike (SmoothPartitionOfUnity ι I M s) ι (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)