smul_C2_1_2

lemma smul_C2_1_2 (m : ℝ) {n k : ℝ} (hk : 0 < k) (hp : 𝓘 p ≠ 𝓘 p') (hl : smul n p ≤ smul k p') :    smul (n + C2_1_2 a * m) p ≤ smul m p' := by  replace hp : 𝓘 p < 𝓘 p' := hl.1.lt_of_ne hp  have : ball_(p') (𝒬 p') m ⊆ ball_(p) (𝒬 p) (n + C2_1_2 a * m) := fun x hx ↦ by    rw [@mem_ball] at hx ⊢    calc      _ ≤ dist_(p) x (𝒬 p') + dist_(p) (𝒬 p') (𝒬 p) := dist_triangle ..      _ ≤ C2_1_2 a * dist_(p') x (𝒬 p') + dist_(p) (𝒬 p') (𝒬 p) := by        gcongr; exact Grid.dist_strictMono hp      _ < C2_1_2 a * m + dist_(p) (𝒬 p') (𝒬 p) := by gcongr; rw [C2_1_2]; positivity      _ < _ := by        rw [add_comm]; gcongr        exact mem_ball.mp <| mem_of_mem_of_subset (by convert! mem_ball_self hk) hl.2  exact ⟨hl.1, this⟩