TileStructure.Forest.limited_scale_impact_first_estimate

lemma limited_scale_impact_first_estimate (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)    (h : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J))) : s J ≤ 𝔰 p := by  by_contra! contr  apply Int.not_le.mpr contr  apply Int.sub_one_lt_iff.mp  apply Int.sub_lt_of_sub_lt  rify  apply lt_of_le_of_lt (hbc := calculation_logD_64 (X := X))  apply tsub_le_iff_left.mpr  have DIsOne := one_lt_realD X  rw [    ← Real.logb_rpow (b := D) (x := 𝔰 p) (by positivity) (by linarith),    ← Real.logb_mul (by positivity) (by positivity),    ← Real.logb_rpow (b := D) (x := s J) (by positivity) (by linarith)  ]  apply (Real.logb_le_logb DIsOne (by positivity) (by positivity)).mpr  have bigger : D ^ (s J) / 8 + 8 * D ^ (𝔰 p) ≥ D ^ s J / (4 : ℝ) := by    rw [not_disjoint_iff] at h    rcases h with ⟨middleX, h1, h2⟩    calc (D ^ s J / (4 : ℝ))    _ ≤ dist (c J) (𝔠 p) := by      apply IF_disjoint_with_ball_THEN_distance_bigger_than_radius (p := 𝔠 p) (belongs := Grid.c_mem_Grid)      have inter_1 : (J : Set X) ∩ ball (c J) (D ^ s J / 4) = ball (c J) (D ^ s J / 4) := inter_eq_self_of_subset_right ball_subset_Grid      have inter_2 : (𝓘 u₁ : Set X) ∩ J = J := inter_eq_self_of_subset_right hJ.2.1      rw [← inter_1, ← inter_2]      apply Disjoint.inter_left      apply Disjoint.inter_left      rw [disjoint_comm]      by_contra notDisjoint      apply hp.2      apply overlap_implies_distance hu₁ hu₂ hu h2u (hpu₁ := notDisjoint)      right      exact hp.1    _ ≤ dist (𝔠 p) middleX + dist middleX (c J) := by      rw [dist_comm]      exact dist_triangle ..    _ ≤ 8 * D ^ (𝔰 p) + dist middleX (c J) := by      gcongr      rw [mem_ball, dist_comm] at h1      exact le_of_lt h1    _ ≤ D ^ (s J) / 8 + 8 * D ^ (𝔰 p) := by      rw [add_comm]      gcongr      rw [mem_ball, ← div_eq_inv_mul] at h2      exact le_of_lt h2  apply le_neg_add_iff_le.mp  have := mul_le_mul_of_nonneg_left (a := 8) (sub_nonneg_of_le bigger) (by positivity)  ring_nf at this  norm_cast