∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F},
  ContDiff ℝ 1 f → dimH (Set.range f) ≤ ↑(Module.finrank ℝ E)