TileStructure.Forest.scales_impacting_interval

lemma scales_impacting_interval (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (hp : p ∈ t u₁ ∪ (t u₂ ∩ 𝔖₀ t u₁ u₂))    (h : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J))) : s J ≤ 𝔰 p := by  obtain ⟨hJLeft, -⟩ := hJ  apply 𝓙_subset_𝓙₀ at hJLeft  rw [mem_union] at hp  have belongs : p ∈ 𝔖₀ t u₁ u₂ := by    cases hp with    | inl h1 => exact 𝔗_subset_𝔖₀ hu₁ hu₂ hu h2u h1    | inr h2 => exact h2.2  cases hJLeft with  | inl scaleVerySmall => exact scaleVerySmall ▸ scale_mem_Icc.1  | inr noGridInBall =>    have pGridIsNotInBall := noGridInBall p belongs    rw [not_subset] at pGridIsNotInBall    obtain ⟨x, ⟨xInTile, xIsNotInBall⟩⟩ := pGridIsNotInBall    rw [mem_ball'] at xIsNotInBall; contrapose! xIsNotInBall; rw [dist_comm]    calc      _ ≤ dist x (𝔠 p) + dist (𝔠 p) (c J) := dist_triangle ..      _ < 4 * D ^ 𝔰 p + 8 * D ^ 𝔰 p + 16 * D ^ s J := by        rw [add_assoc]; gcongr        · exact mem_ball.mp (Grid_subset_ball xInTile)        · exact dist_lt_of_not_disjoint_ball h      _ ≤ 4 * D ^ s J + 8 * D ^ s J + 16 * D ^ s J := by gcongr <;> exact one_le_realD a      _ ≤ _ := by        rw [← add_mul, ← add_mul, zpow_add_one₀ (realD_pos a).ne', mul_comm _ (D : ℝ),          ← mul_assoc]; gcongr        calc          _ ≤ 100 * (1 : ℝ) := by norm_num          _ ≤ _ := by gcongr; exact one_le_realD a