integer_ball_cover

lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R} :    CoveredByBalls (ball f (2 * R')) 3 R' := by  unfold WithFunctionDistance at f  rw [coveredByBalls_iff]  by_cases! R'pos : 0 ≥ R'  · -- trivial case    refine ⟨{f}, Finset.card_singleton f ▸ by norm_num, ?_⟩    have hunion : (⋃ x_1 ∈ ({f} : Finset (WithFunctionDistance x R)), ball_{x, R} x_1 R') = ball_{x, R} f R' := by      ext y      simp only [Set.mem_iUnion, exists_prop]      constructor      · rintro ⟨i, hi, hb⟩; rwa [Finset.mem_singleton.mp hi] at hb      · intro h; exact ⟨f, Finset.mem_singleton_self f, h⟩    rw [hunion, Metric.ball_eq_empty.mpr R'pos, Set.subset_empty_iff, Metric.ball_eq_empty]    linarith  by_cases! Rpos : 0 ≥ R  · -- trivial case    refine ⟨{f}, Finset.card_singleton f ▸ by norm_num, ?_⟩    have hunion : (⋃ x_1 ∈ ({f} : Finset (WithFunctionDistance x R)), ball_{x, R} x_1 R') = ball_{x, R} f R' := by      ext y      simp only [Set.mem_iUnion, exists_prop]      constructor      · rintro ⟨i, hi, hb⟩; rwa [Finset.mem_singleton.mp hi] at hb      · intro h; exact ⟨f, Finset.mem_singleton_self f, h⟩    rw [hunion]    convert Set.subset_univ _    ext g    refine ⟨by simp, ?_⟩    simp only [Set.mem_univ, mem_ball, true_implies, dist_integer_linear_eq]    convert! R'pos    simpa using Or.inl Rpos  set m₁ := Int.floor (f - R' / (2 * R)) with m₁def  set! m₂ := f with m₂def  set m₃ := Int.ceil (f + R' / (2 * R)) with m₃def  /- classical is necessary to be able to build a Finset of WithFunctionDistance. -/  classical  set balls : Finset (WithFunctionDistance x R) := {m₁, m₂, m₃} with balls_def  use balls  constructor  · rw [balls_def]    apply Finset.card_le_three  intro φ hφ  unfold WithFunctionDistance at φ  rw [mem_ball, dist_comm] at hφ  /- m₁, m₂, m₃ each correspond to one case. -/  simp only [Set.mem_iUnion, mem_ball, exists_prop]  by_cases! h : φ ≤ f - R' / (2 * R)  · use m₁    constructor    · apply Finset.mem_insert_self    rw [dist_integer_linear_eq]    calc 2 * max R 0 * |↑φ - ↑m₁|      _ = 2 * R * |↑φ - ↑m₁| := by        congr        rw [max_eq_left_iff]        exact Rpos.le      _ = 2 * R * (m₁ - ↑φ) := by        rw [abs_of_nonpos]        on_goal 1 => simp only [neg_sub]        norm_cast        simp only [tsub_le_iff_right, zero_add]        rwa [m₁def, Int.le_floor]      _ = 2 * R * (m₁ - f) + 2 * R * (f - φ) := by ring      _ < - R' + 2 * R' := by        apply add_lt_add_of_le_of_lt        · rw [m₁def]          calc 2 * R * (⌊f - R' / (2 * R)⌋ - f)            _ ≤ 2 * R * (f - R' / (2 * R) - f) := by              gcongr              apply Int.floor_le            _ = -R' := by              ring_nf              rw [mul_comm, ←mul_assoc, inv_mul_cancel₀ Rpos.ne.symm, one_mul]        · calc 2 * R * (↑f - ↑φ)            _ ≤ 2 * R * |↑f - ↑φ| := by              gcongr              apply le_abs_self            _ < 2 * R' := by              convert hφ              rw [dist_integer_linear_eq]              congr              symm              rw [max_eq_left_iff]              exact Rpos.le      _ = R' := by ring  by_cases! h' : φ < f + R' / (2 * R)  · use m₂    constructor    · exact Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self m₂ _))    rw [m₂def, dist_comm]    rw [dist_integer_linear_eq]    calc 2 * max R 0 * |↑f - ↑φ|      _ = 2 * R * |↑f - ↑φ| := by        congr        rw [max_eq_left_iff]        exact Rpos.le      _ < 2 * R * (R' / (2 * R)) := by        gcongr        rw [abs_sub_lt_iff]        constructor <;> linarith      _ = R' := by field_simp  use m₃  constructor  · apply Finset.mem_insert.mpr; right    apply Finset.mem_insert.mpr; right    exact Finset.mem_singleton.mpr m₃def  rw [dist_integer_linear_eq]  calc 2 * max R 0 * |↑φ - ↑m₃|    _ = 2 * R * (↑φ - ↑m₃) := by      rw [abs_of_nonneg]      · congr        rw [max_eq_left_iff]        exact Rpos.le      simp only [sub_nonneg, Int.cast_le]      rwa [m₃def, Int.ceil_le]    _ = 2 * R * (φ - f) + 2 * R * (f - m₃) := by ring    _ < 2 * R' - R' := by      apply add_lt_add_of_lt_of_le      · calc 2 * R * (↑φ - ↑f)          _ ≤ 2 * R * |↑φ - ↑f| := by            gcongr            exact le_abs_self _          _ = 2 * R * |↑f - ↑φ| := by            congr 1            exact abs_sub_comm _ _          _ < 2 * R' := by            convert hφ            rw [dist_integer_linear_eq]            congr            symm            rw [max_eq_left_iff]            exact Rpos.le      · rw [m₃def]        calc 2 * R * (f - ⌈f + R' / (2 * R)⌉)          _ ≤ 2 * R * (f - (f + R' / (2 * R))) := by            gcongr            exact Int.le_ceil _          _ = -R' := by            ring_nf            rw [mul_comm, ←mul_assoc, inv_mul_cancel₀ Rpos.ne.symm, one_mul]    _ = R' := by ring