Lemmas about interaction of ball and homothety

TODO Generalise these lemmas appropriately.

@[simp]

theorem norm_coe_ball_lt {F : Type u_1} [NormedAddCommGroup F] (r : ℝ) (x : ↑(Metric.ball 0 r)) : ‖↑x‖ < r

theorem mapsTo_homothety_ball {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (c : F) {r : ℝ} (hr : 0 < r) : Set.MapsTo (fun (y : F) => (AffineMap.homothety c r⁻¹) y -ᵥ c) (Metric.ball c r) (Metric.ball 0 1)

theorem contDiff_homothety {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (c : F) (r : ℝ) : ContDiff ℝ ↑n ⇑(AffineMap.homothety c r)