TileStructure.Forest.thin_scale_impact

lemma thin_scale_impact (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))) :    𝔰 p ≤ s J - C7_6_3 a n := by  by_contra! h  have bZn : 4 ≤ Z * (n + 1) := by    rw [← mul_one 4]; gcongr    · exact four_le_Z (X := X)    · exact Nat.le_add_left ..  have key := thin_scale_impact_key hu₁ hu₂ hu h2u hp hJ hd h  rw [← Real.rpow_natCast, ← Real.rpow_add zero_lt_two,    Real.rpow_lt_rpow_left_iff one_lt_two, Nat.cast_sub (by lia), Nat.cast_mul, Nat.cast_add,    Nat.cast_one, mul_add_one] at key  nth_rw 1 [← add_halves ((Z : ℝ) * n)] at key  rw [add_rotate, ← sub_add_eq_add_sub, add_lt_add_iff_right, C7_6_3, sub_add_cancel] at key  have : (2 * 𝕔 + 2 : ℝ) ≠ 0 := by norm_cast  have : (a : ℝ) ≠ 0 := by norm_cast; linarith [four_le_a X]  have rearr : (a : ℝ) * (𝕔 * a ^ 2 * (Z * n / ((2 * 𝕔 + 2) * a ^ 3) + 1) + 9) =      Z * n / 2 * (𝕔 / (𝕔 + 1)) * a ^ 3 / a ^ 3 + 𝕔 * a ^ 3 + 9 * a := by        field_simp  have fla := four_le_a X  rw [rearr, mul_div_cancel_right₀ _ (by norm_cast; positivity), add_assoc,    ← sub_lt_iff_lt_add', sub_right_comm, add_sub_right_comm, ← mul_one_sub, div_mul_comm,    show (1 - 𝕔 / (𝕔 + 1)) / (2 : ℝ) = 1 / (2 * 𝕔 + 2) by field_simp; ring,    sub_lt_iff_lt_add] at key  apply absurd key; rw [not_lt]  suffices 𝕔 * a ^ 3 + 9 * a + 1 ≤ (Z : ℝ) by    apply this.trans; nth_rw 1 [← zero_add (Z : ℝ)]; gcongr; positivity  norm_cast; rw [defaultZ]  calc    _ = 𝕔 * a ^ 3 + 9 * a * 1 * 1 + 1 * 1 * 1 * 1 := by norm_num    _ ≤ 𝕔 * a ^ 3 + 9 * a * a * a + 1 * a * a * a := by gcongr <;> lia    _ = (𝕔 + 10) * a ^ 3 := by ring    _ ≤ 2 ^ (7 + 3 * a) := by      rw [pow_add, pow_mul']; gcongr; exacts [by linarith [c_le_100], Nat.lt_two_pow_self.le]    _ ≤ _ := by gcongr <;> lia