TileStructure.Forest.thin_scale_impact_key

lemma thin_scale_impact_key (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₆ t u₁)    (hd : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8 * D ^ s J)))    (h : s J - C7_6_3 a n < 𝔰 p) :    (2 : ℝ) ^ (Z * (n + 1) - 1) <    2 ^ (a * (𝕔 * a ^ 2 * (C7_6_3 a n + 2 + 1) + 9)) * 2 ^ ((Z : ℝ) * n / 2) := by  obtain ⟨b1, ⟨J', lJ', sJ', ⟨p', mp', sp'⟩⟩⟩ := thin_scale_impact_prelims hu₁ hJ hd h  have bZn : 4 ≤ Z * (n + 1) := by    rw [← mul_one 4]; gcongr    · exact four_le_Z (X := X)    · exact Nat.le_add_left ..  calc    _ ≤ (2 : ℝ) ^ (Z * (n + 1)) - 4 := by      nth_rw 2 [← Nat.sub_add_cancel (show 1 ≤ Z * (n + 1) by lia)]      rw [pow_succ, mul_two, add_sub_assoc, ← neg_add_le_iff_le_add, neg_add_cancel, sub_nonneg,        show (4 : ℝ) = 2 ^ 2 by norm_num]      apply pow_le_pow_right₀ one_le_two; lia    _ < dist_(p') (𝒬 u₁) (𝒬 u₂) := by      refine (sub_lt_sub (t.lt_dist hu₂ hu₁ hu.symm mp' ((t.𝓘_le_𝓘 hu₁ mp').trans h2u))        (t.dist_lt_four hu₁ mp')).trans_le ((le_abs_self _).trans ?_)      simp_rw [dist_comm, abs_sub_comm]; exact abs_dist_sub_le ..    _ ≤ dist_{𝔠 p, 128 * D ^ (𝔰 p + C7_6_3 a n + 2)} (𝒬 u₁) (𝒬 u₂) := by      refine cdist_mono (ball_subset_Grid.trans sp' |>.trans (ball_subset_ball' ?_))      calc        _ ≤ (100 : ℝ) * D ^ (s J' + 1) + dist (c J') (c J) + dist (𝔠 p) (c J) := by          rw [add_assoc]; gcongr; exact dist_triangle_right ..        _ ≤ (100 : ℝ) * D ^ (s J' + 1) + 4 * D ^ s J' + 16 * D ^ (𝔰 p + C7_6_3 a n + 2) := by          gcongr; · exact (mem_ball'.mp (Grid_subset_ball (lJ'.1.1 Grid.c_mem_Grid))).le        _ ≤ (100 : ℝ) * D ^ (𝔰 p + C7_6_3 a n + 2) + 4 * D ^ (𝔰 p + C7_6_3 a n + 2) +            16 * D ^ (𝔰 p + C7_6_3 a n + 2) := by          rw [← sub_eq_iff_eq_add] at sJ'          rw [← sJ', Int.cast_sub, Int.cast_one, sub_lt_iff_lt_add, sub_lt_iff_lt_add] at h          simp_rw [← Real.rpow_intCast, Int.cast_add, Int.cast_one]          gcongr 100 * (D : ℝ) ^ ?_ + 4 * D ^ ?_ + _          exacts [one_le_realD _, by linarith only [h], one_le_realD _, by linarith only [h]]        _ ≤ _ := by rw [← add_mul, ← add_mul]; gcongr; norm_num    _ ≤ dist_{𝔠 p, 2 ^ (𝕔 * a ^ 2 * ⌈C7_6_3 a n + 2⌉₊ + 9) * (D ^ 𝔰 p / 4)} (𝒬 u₁) (𝒬 u₂) := by      refine cdist_mono (ball_subset_ball ?_)      rw [add_assoc, Real.rpow_add (by simp), Real.rpow_intCast,        show (128 : ℝ) * (D ^ 𝔰 p * D ^ (C7_6_3 a n + 2)) =          D ^ (C7_6_3 a n + 2) * 2 ^ 9 * (D ^ 𝔰 p / 4) by ring]      refine mul_le_mul_of_nonneg_right ?_ (by positivity)      rw [pow_add, pow_mul _ (𝕔 * a ^ 2), defaultD, ← Real.rpow_natCast _ ⌈_⌉₊, Nat.cast_pow,        Nat.cast_ofNat]; gcongr      · exact_mod_cast Nat.one_le_two_pow      · exact Nat.le_ceil _    _ ≤ (defaultA a) ^ (𝕔 * a ^ 2 * ⌈C7_6_3 a n + 2⌉₊ + 9) * dist_(p) (𝒬 u₁) (𝒬 u₂) :=      cdist_le_iterate (by unfold defaultD; positivity) ..    _ ≤ _ := by      obtain ⟨hp₁, hp₂⟩ := hp      simp_rw [𝔖₀, mem_setOf, not_and_or, mem_union, hp₁, or_true, not_true_eq_false,        false_or, not_le] at hp₂      simp_rw [defaultA, Nat.cast_pow, Nat.cast_ofNat, ← pow_mul, ← Real.rpow_natCast 2]      push_cast; gcongr      · exact one_le_two      · exact (Nat.ceil_lt_add_one nonneg_C7_6_3_add_two).le