{ι : 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} →
                    {inst_5 : FiniteDimensional ℝ E} →
                      {s : optParam (Set M) Set.univ} →
                        {P : Sort u} →
                          {c : ι → M} →
                            {toFun : (i : ι) → SmoothBumpFunction I (c i)} →
                              {c_mem' : ∀ (i : ι), c i ∈ s} →
                                {locallyFinite' : LocallyFinite fun i => Function.support ↑(toFun i)} →
                                  {eventuallyEq_one' : ∀ x ∈ s, ∃ i, ↑(toFun i) =ᶠ[nhds x] 1} →
                                    {c' : ι → M} →
                                      {toFun' : (i : ι) → SmoothBumpFunction I (c' i)} →
                                        {c_mem'' : ∀ (i : ι), c' i ∈ s} →
                                          {locallyFinite'' : LocallyFinite fun i => Function.support ↑(toFun' i)} →
                                            {eventuallyEq_one'' : ∀ x ∈ s, ∃ i, ↑(toFun' i) =ᶠ[nhds x] 1} →
                                              { c := c, toFun := toFun, c_mem' := c_mem',
                                                    locallyFinite' := locallyFinite',
                                                    eventuallyEq_one' := eventuallyEq_one' } =
                                                  { c := c', toFun := toFun', c_mem' := c_mem'',
                                                    locallyFinite' := locallyFinite'',
                                                    eventuallyEq_one' := eventuallyEq_one'' } →
                                                (c ≍ c' → toFun ≍ toFun' → P) → P