{ι : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {s : Set X} →
        {motive : PartitionOfUnity ι X s → Sort u} →
          (t : PartitionOfUnity ι X s) →
            ((toFun : ι → C(X, ℝ)) →
                (locallyFinite' : LocallyFinite fun i => Function.support ⇑(toFun i)) →
                  (nonneg' : 0 ≤ toFun) →
                    (sum_eq_one' : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun i) x = 1) →
                      (sum_le_one' : ∀ (x : X), ∑ᶠ (i : ι), (toFun i) x ≤ 1) →
                        motive
                          { toFun := toFun, locallyFinite' := locallyFinite', nonneg' := nonneg',
                            sum_eq_one' := sum_eq_one', sum_le_one' := sum_le_one' }) →
              motive t