∀ {ι : 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 : optParam (Set M) Set.univ} [inst_5 : SizeOf ι] [inst_6 : SizeOf E]
  [inst_7 : SizeOf H] [inst_8 : SizeOf M] [inst_9 : (a : M) → SizeOf (s a)]
  (toFun : ι → ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)
  (locallyFinite' : LocallyFinite fun i => Function.support ⇑(toFun i)) (nonneg' : ∀ (i : ι) (x : M), 0 ≤ (toFun i) x)
  (sum_eq_one' : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun i) x = 1) (sum_le_one' : ∀ (x : M), ∑ᶠ (i : ι), (toFun i) x ≤ 1),
  sizeOf
      { toFun := toFun, locallyFinite' := locallyFinite', nonneg' := nonneg', sum_eq_one' := sum_eq_one',
        sum_le_one' := sum_le_one' } =
    1