Antichain.tile_reach

lemma tile_reach {ϑ : Θ X} {N : ℕ} {p p' : 𝔓 X} (hp : dist_(p) (𝒬 p) ϑ ≤ 2 ^ N)    (hp' : dist_(p') (𝒬 p') ϑ ≤ 2 ^ N) (hI : 𝓘 p ≤ 𝓘 p') (hs : 𝔰 p < 𝔰 p') :    smul (2^(N + 2)) p ≤ smul (2^(N + 2)) p' := by  -- Ineq. 6.3.4  have hp2 : dist_(p) ϑ (𝒬 p') ≤ 2^N := by rw [dist_comm]; exact le_trans (Grid.dist_mono hI) hp'  -- Ineq. 6.3.5  have hp'2 : dist_(p) (𝒬 p) (𝒬 p') ≤ 2^(N + 1) :=    calc dist_(p) (𝒬 p) (𝒬 p')      _ ≤ dist_(p) (𝒬 p) ϑ + dist_(p) ϑ (𝒬 p') := dist_triangle ..      _ ≤ 2^N + 2^N := add_le_add hp hp2      _ = 2^(N + 1) := by ring  -- Start proof of ineq. 6.3.3.  simp only [TileLike.le_def, smul_fst, smul_snd]  refine ⟨hI, fun o' ho' ↦ ?_⟩ -- o' is ϑ' in blueprint, ho' is eq. 6.3.6.  -- Ineq. 6.3.7  have hlt : dist_{𝔠 p', 8 * D^𝔰 p'} (𝒬 p') o' < 2^(5*a + N + 2) := by    have hle : dist_{𝔠 p', 8 * D^𝔰 p'} (𝒬 p') o' ≤ (defaultA a) ^ 5 * dist_(p') (𝒬 p') o' := by      have hpos : (0 : ℝ) < D^𝔰 p'/4 := by        rw [div_eq_mul_one_div, mul_comm]        apply mul_defaultD_pow_pos _ (by linarith)      have h8 : (8 : ℝ) * D^𝔰 p' = 2^5 * (D^𝔰 p'/4) := by ring      exact h8 ▸ cdist_le_iterate hpos (𝒬 p') o' 5    apply lt_of_le_of_lt hle    simp only [defaultA, add_assoc]    rw [pow_add, Nat.cast_pow, Nat.cast_ofNat, ← pow_mul, mul_comm a, dist_comm]    gcongr    exact ho'  -- Claim 6.3.8  have hin : 𝔠 p ∈ ball (𝔠 p') (4 * D^𝔰 p') := Grid_subset_ball (hI.1 Grid.c_mem_Grid)  -- Claim 6.3.9  have hball_le : ball (𝔠 p) (4 * D^𝔰 p') ⊆ ball (𝔠 p') (8 * D^𝔰 p') := by    intro x hx    rw [mem_ball] at hx hin ⊢    calc dist x (𝔠 p')      _ ≤ dist x (𝔠 p)  + dist (𝔠 p) (𝔠 p') := dist_triangle _ _ _      _ < 4 * ↑D ^ 𝔰 p' + 4 * ↑D ^ 𝔰 p' := add_lt_add hx hin      _ = 8 * ↑D ^ 𝔰 p' := by ring  -- Ineq. 6.3.10  have hlt2 : dist_{𝔠 p, 4 * D^𝔰 p'} (𝒬 p') o' < 2^(5*a + N + 2) :=    lt_of_le_of_lt (cdist_mono hball_le) hlt  -- Ineq. 6.3.11  have hlt3 : dist_{𝔠 p, 2^((2 : ℤ) - 5*a^2 - 2*a) * D^𝔰 p'} (𝒬 p') o' < 2^N := by    have hle : 2 ^ ((5 : ℤ)*a + 2) * dist_{𝔠 p, 2^((2 : ℤ) - 5*a^2 - 2*a) * D^𝔰 p'} (𝒬 p') o' ≤        dist_{𝔠 p, 4 * D^𝔰 p'} (𝒬 p') o' := by      have heq : (defaultA a : ℝ) ^ ((5 : ℤ)*a + 2) * 2^((2 : ℤ) - 5*a^2 - 2*a) = 4 := by        simp only [defaultA, Nat.cast_pow, Nat.cast_ofNat, ← zpow_natCast, ← zpow_mul]        rw [← zpow_add₀ two_ne_zero]        ring_nf        norm_num      rw [← heq, mul_assoc]      exact le_cdist_iterate (by positivity) (𝒬 p') o' (5*a + 2)    rw [← le_div_iff₀' (by positivity), div_eq_mul_inv, ← zpow_neg, neg_add, ← neg_mul,      ← sub_eq_add_neg, mul_comm _ ((2 : ℝ) ^ _)] at hle    calc dist_{𝔠 p, 2^((2 : ℤ) - 5*a^2 - 2*a) * D^𝔰 p'} (𝒬 p') o'      _ ≤ 2^(-(5 : ℤ)*a - 2) * dist_{𝔠 p, 4 * D^𝔰 p'} (𝒬 p') o' := hle      _ < 2^(-(5 : ℤ)*a - 2) * 2^(5*a + N + 2) := (mul_lt_mul_iff_right₀ (by positivity)).mpr hlt2      _ = 2^N := by        rw [← zpow_natCast, ← zpow_add₀ two_ne_zero]        simp  -- Ineq. 6.3.12  have hp'3 : dist_(p) (𝒬 p') o' < 2^N := by    apply lt_of_le_of_lt (cdist_mono _) hlt3    gcongr    rw [div_le_iff₀ (by positivity), mul_comm, ← mul_assoc]    calc (D : ℝ) ^ 𝔰 p      _ = 1 * (D : ℝ) ^ 𝔰 p := by rw [one_mul]      _ ≤ 4 * 2 ^ (2 - 5 * (a : ℤ) ^ 2 - 2 * ↑a) * D * D ^ 𝔰 p := by        have h4 : (4 : ℝ) = 2^(2 : ℤ) := by ring        apply mul_le_mul _ (le_refl _) (by positivity) (by positivity)        · have h12 : (1 : ℝ) ≤ 2 := one_le_two          simp only [defaultD, Nat.cast_pow, Nat.cast_ofNat]          rw [h4, ← zpow_natCast, ← zpow_add₀ two_ne_zero, ← zpow_add₀ two_ne_zero, ← zpow_zero 2]          rw [Nat.cast_mul, Nat.cast_pow]          gcongr --uses h12          suffices (2 : ℤ) * a + 5 * a ^ 2 ≤ 𝕔 * a ^ 2 by linarith          norm_cast          calc 2 * a + 5 * a ^ 2          _ ≤ a * a + 5 * a ^ 2 := by gcongr; linarith [four_le_a X]          _ = 6 * a ^ 2 := by ring          _ ≤ 𝕔 * a ^ 2 := by gcongr; linarith [seven_le_c]      _ = (4 * 2 ^ (2 - 5 * (a : ℤ)  ^ 2 - 2 * ↑a)) * (D * D ^ 𝔰 p) := by ring      _ ≤ 4 * 2 ^ (2 - 5 * (a : ℤ)  ^ 2 - 2 * ↑a) * D ^ 𝔰 p' := by        have h1D : 1 ≤ (D : ℝ) := one_le_realD _        nth_rewrite 1 [mul_le_mul_iff_right₀ (by positivity), ← zpow_one (D : ℝ),          ← zpow_add₀ (ne_of_gt (realD_pos _))]        gcongr        rw [add_comm]        exact hs  -- Ineq. 6.3.13 (and ineq. 6.3.3.)  have h34 : (3 : ℝ) < 4 := by linarith  calc dist_(p) o' (𝒬 p)    _ = dist_(p) (𝒬 p) o' := by rw [dist_comm]    _ ≤ dist_(p) (𝒬 p) (𝒬 p') + dist_(p) (𝒬 p') o' := dist_triangle _ _ _    _ < 2^(N + 1) + 2^N := add_lt_add_of_le_of_lt hp'2 hp'3    _ < 2^(N + 2) := by ring_nf; gcongr