TileStructure.Forest.le_of_mem_E

lemma le_of_mem_E {y : X} (hy : y ∈ E p) (hx' : x' ∉ ball (𝔠 p) (5 * D ^ 𝔰 p)) :    2 - 4 * ((D : ℝ) ^ (-𝔰 p) * dist y x) ≤ dist x x' / D ^ (𝔰 p) * 4 := by  have := one_le_realD a  calc    _ ≤ 2 - 4 * (D : ℝ) ^ (-𝔰 p) * (dist x (𝔠 p) - dist y (𝔠 p)) := by      rw [mul_assoc]; gcongr; rw [sub_le_iff_le_add]; exact dist_triangle_left ..    _ ≤ 2 - 4 * (D : ℝ) ^ (-𝔰 p) * dist x (𝔠 p) + 16 := by      rw [mul_sub, sub_add]; gcongr; rw [mul_rotate, show (16 : ℝ) = 4 * 4 by norm_num]; gcongr      rw [zpow_neg, inv_mul_le_iff₀' (by positivity)]      exact (mem_ball.mp ((E_subset_𝓘.trans Grid_subset_ball) hy)).le    _ = 4 * (D : ℝ) ^ (-𝔰 p) * (5 * D ^ 𝔰 p - dist x (𝔠 p)) - 2 := by      rw [mul_sub, show 4 * (D : ℝ) ^ (-𝔰 p) * (5 * D ^ 𝔰 p) = 20 * (D ^ 𝔰 p * D ^ (-𝔰 p)) by ring,        ← zpow_add₀ (by positivity), add_neg_cancel, zpow_zero, mul_one]; ring    _ ≤ 4 * (D : ℝ) ^ (-𝔰 p) * (dist x' (𝔠 p) - dist x (𝔠 p)) - 2 := by      gcongr; rwa [mem_ball, not_lt] at hx'    _ ≤ 4 * (D : ℝ) ^ (-𝔰 p) * dist x x' - 2 := by      gcongr; rw [sub_le_iff_le_add]; exact dist_triangle_left ..    _ ≤ _ := by rw [zpow_neg, mul_rotate, inv_mul_eq_div]; norm_num