{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} →
                    {P : Sort u} →
                      {toContDiffBump : ContDiffBump (↑(extChartAt I c) c)} →
                        {closedBall_subset :
                            Metric.closedBall (↑(extChartAt I c) c) toContDiffBump.rOut ∩ Set.range ↑I ⊆
                              (extChartAt I c).target} →
                          {toContDiffBump' : ContDiffBump (↑(extChartAt I c) c)} →
                            {closedBall_subset' :
                                Metric.closedBall (↑(extChartAt I c) c) toContDiffBump'.rOut ∩ Set.range ↑I ⊆
                                  (extChartAt I c).target} →
                              { toContDiffBump := toContDiffBump, closedBall_subset := closedBall_subset } =
                                  { toContDiffBump := toContDiffBump', closedBall_subset := closedBall_subset' } →
                                (toContDiffBump ≍ toContDiffBump' → P) → P