∀ {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}
  (toContDiffBump : ContDiffBump (↑(extChartAt I c) c))
  (closedBall_subset :
    Metric.closedBall (↑(extChartAt I c) c) toContDiffBump.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target)
  (toContDiffBump_1 : ContDiffBump (↑(extChartAt I c) c))
  (closedBall_subset_1 :
    Metric.closedBall (↑(extChartAt I c) c) toContDiffBump_1.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target),
  ({ toContDiffBump := toContDiffBump, closedBall_subset := closedBall_subset } =
      { toContDiffBump := toContDiffBump_1, closedBall_subset := closedBall_subset_1 }) =
    (toContDiffBump = toContDiffBump_1)