Sort 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] →
                    {c : M} →
                      SmoothBumpFunction I c →
                        {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'] → {c' : M'} → SmoothBumpFunction I' c' → Sort u