TileStructure.Forest.moderate_scale_change

lemma moderate_scale_change (hJ : J ∈ 𝓙₅ t u₁ u₂) (hJ' : J' ∈ 𝓙₅ t u₁ u₂)    (hd : ¬Disjoint (ball (c J) (8 * D ^ s J)) (ball (c J') (8 * D ^ s J'))) :    s J - 1 ≤ s J' := by  by_contra! hs  have fa : ∀ p ∈ t.𝔖₀ u₁ u₂, ¬↑(𝓘 p) ⊆ ball (c J) (100 * D ^ (s J + 1)) :=    hJ.1.1.resolve_left (by linarith [(scale_mem_Icc (i := J')).1])  apply absurd fa; push Not  obtain ⟨J'', sJ'', lJ''⟩ : ∃ J'', s J'' = s J' + 1 ∧ J' ≤ J'' := by    refine Grid.exists_supercube (s J' + 1) ⟨by lia, ?_⟩    rw [lt_sub_iff_add_lt] at hs; exact hs.le.trans scale_mem_Icc.2  obtain ⟨p, mp, sp⟩ : ∃ p ∈ t.𝔖₀ u₁ u₂, ↑(𝓘 p) ⊆ ball (c J'') (100 * D ^ (s J' + 1 + 1)) := by    have : J'' ∉ 𝓙₀ (t.𝔖₀ u₁ u₂) := bigger_than_𝓙_is_not_in_𝓙₀ lJ'' (by linarith) hJ'.1    rw [𝓙₀, mem_setOf_eq, sJ''] at this; push Not at this; exact this.2  use p, mp, sp.trans (ball_subset_ball' ?_)  calc    _ ≤ 100 * D ^ (s J' + 1 + 1) + (dist (c J'') (c J') + dist (c J) (c J')) :=      add_le_add_right (dist_triangle_right ..) _    _ ≤ 100 * D ^ (s J' + 1 + 1) + (4 * D ^ s J'' + 8 * D ^ s J + 8 * D ^ s J') := by      rw [add_assoc (4 * _)]; gcongr      · exact (mem_ball'.mp (Grid_subset_ball (lJ''.1 Grid.c_mem_Grid))).le      · exact (dist_lt_of_not_disjoint_ball hd).le    _ ≤ 100 * D ^ s J + (4 * D ^ s J + 8 * D ^ s J + 8 * D ^ s J) := by      gcongr; exacts [one_le_realD a, by lia, one_le_realD a, by lia, one_le_realD a, by lia]    _ ≤ _ := by      rw [← add_mul, ← add_mul, ← add_mul, zpow_add_one₀ (by simp), mul_comm _ (D : ℝ), ← mul_assoc]      gcongr; trans 100 * 4      · norm_num      · gcongr; exact four_le_realD X