TileStructure.Forest.quarter_add_two_mul_D_mul_card_le

lemma quarter_add_two_mul_D_mul_card_le (hJ : J ∈ 𝓙₅ t u₁ u₂) :    1 / 4 + 2 * (D : ℝ) * {J' ∈ (𝓙₅ t u₁ u₂).toFinset |      ¬Disjoint (ball (c J) (8 * D ^ s J)) (ball (c J') (8 * D ^ s J'))}.card ≤ C7_5_2 a := by  set V := {J' ∈ (𝓙₅ t u₁ u₂).toFinset |      ¬Disjoint (ball (c J) (8 * D ^ s J)) (ball (c J') (8 * D ^ s J'))}  suffices V.card ≤ 2 ^ (2 * 𝕔 * a ^ 3 + 7 * a) by    calc      _ ≤ 1 / 4 + 2 * (D : ℝ) * 2 ^ (2 * 𝕔 * a ^ 3 + 7 * a) := by gcongr; norm_cast      _ ≤ 2 ^ (𝕔 * a ^ 2 + 1 + (2 * 𝕔 * a ^ 3 + 7 * a)) +          2 ^ (𝕔 * a ^ 2 + 1 + (2 * 𝕔 * a ^ 3 + 7 * a)) := by        rw [defaultD, Nat.cast_pow, Nat.cast_ofNat, ← pow_succ', ← pow_add]        gcongr; trans 1        · norm_num        · norm_cast; exact Nat.one_le_two_pow      _ ≤ _ := by        rw [C7_5_2]        norm_cast        apply add_le_pow_two le_rfl le_rfl ?_        have := four_le_a X        ring_nf        suffices 𝕔 * a ^ 2 + 7 * a + 2 ≤ a ^ 3 * 2 + a ^ 3 * (𝕔 / 4)  by linarith        calc          _ ≤ (4 * (𝕔 / 4) + 3) * a ^ 2 + 7 * a + a := by            gcongr            · lia            · linarith          _ = (𝕔 / 4) * 4 * a ^ 2 + 3 * a ^ 2 + 2 * 4 * a := by ring          _ ≤ (𝕔 / 4) * a * a ^ 2 + 3 * a ^ 2 + 2 * a * a := by gcongr          _ = (𝕔 / 4) * a ^ 3 + 5 * a ^ 2 := by ring          _ ≤ (𝕔 / 4) * a ^ 3 + 2 * 4 * a ^ 2 := by gcongr; norm_num          _ ≤ (𝕔 / 4) * a ^ 3 + 2 * a * a ^ 2 := by gcongr          _ = _ := by ring  have dbl : ∀ J' ∈ V, volume (ball (c J) (9 * D ^ (s J + 1))) ≤      2 ^ (2 * 𝕔 * a ^ 3 + 7 * a) * volume (ball (c J') (D ^ s J' / 4)) := fun J' mJ' ↦ by    simp_rw [V, Finset.mem_filter, mem_toFinset] at mJ'    have hs := moderate_scale_change hJ mJ'.1 mJ'.2    rw [disjoint_comm] at mJ'    have hs' := moderate_scale_change mJ'.1 hJ mJ'.2    calc      _ ≤ 2 ^ (2 * 𝕔 * a ^ 3) * volume (ball (c J') (18 * D ^ s J')) := by        have db : dist (c J') (c J) + 9 * D ^ (s J + 1) ≤ D ^ 2 * (18 * D ^ s J') :=          calc            _ ≤ 8 * (D : ℝ) ^ s J' + 8 * D ^ s J + 9 * D ^ (s J + 1) := by              gcongr; exact (dist_lt_of_not_disjoint_ball mJ'.2).le            _ ≤ 8 * (D : ℝ) ^ (s J + 1) + D ^ (s J + 1) + 9 * D ^ (s J + 1) := by              gcongr; exacts [one_le_realD a, by lia, by                rw [zpow_add_one₀ (by simp), mul_comm 8]; gcongr; exact eight_le_realD X]            _ ≤ _ := by              rw [← add_one_mul, ← add_mul, ← mul_assoc, ← mul_rotate, ← zpow_natCast,                ← zpow_add₀ (by simp), mul_comm _ 18, show (8 : ℝ) + 1 + 9 = 18 by norm_num]              gcongr 18 * (D : ℝ) ^ ?_; exacts [one_le_realD a, by lia]        convert measure_ball_le_of_dist_le' (μ := volume) (by simp) db        simp_rw [As, defaultA, defaultD, Nat.cast_pow, Nat.cast_ofNat, ← pow_mul, Real.logb_pow,          Real.logb_self_eq_one one_lt_two, mul_one, Nat.ceil_natCast, ENNReal.coe_pow,          ENNReal.coe_ofNat]        ring      _ ≤ 2 ^ (2 * 𝕔 * a ^ 3 + 7 * a) * volume (ball (c J') (18 / 128 * D ^ s J')) := by        nth_rw 1 [show (18 : ℝ) * D ^ s J' = 2 ^ 7 * (18 / 128 * D ^ s J') by ring]        rw [pow_add, mul_assoc, mul_assoc]; gcongr        convert! measure_ball_two_le_same_iterate (μ := volume) (c J') _ 7 using 2        unfold defaultA; norm_cast; rw [← pow_mul']      _ ≤ _ := by rw [div_eq_inv_mul _ 4]; gcongr; norm_num  replace dbl : V.card * volume (ball (c J) (9 * D ^ (s J + 1))) ≤      2 ^ (2 * 𝕔 * a ^ 3 + 7 * a) * volume (ball (c J) (9 * D ^ (s J + 1))) := by    calc      _ ≤ 2 ^ (2 * 𝕔 * a ^ 3 + 7 * a) * ∑ J' ∈ V, volume (ball (c J') (D ^ s J' / 4)) := by        rw [Finset.mul_sum, ← nsmul_eq_mul, ← Finset.sum_const]; exact Finset.sum_le_sum dbl      _ = 2 ^ (2 * 𝕔 * a ^ 3 + 7 * a) * volume (⋃ J' ∈ V, ball (c J') (D ^ s J' / 4)) := by        congr; refine (measure_biUnion_finset ?_ fun _ _ ↦ measurableSet_ball).symm        have Vs : V ⊆ (t.𝓙₅ u₁ u₂).toFinset := Finset.filter_subset ..        rw [subset_toFinset] at Vs        exact (pairwiseDisjoint_𝓙₅.subset Vs).mono fun _ ↦ ball_subset_Grid      _ ≤ _ := by        gcongr; refine iUnion₂_subset fun J' mJ' ↦ ball_subset_ball' ?_        simp_rw [V, Finset.mem_filter, mem_toFinset] at mJ'        have hs := moderate_scale_change hJ mJ'.1 mJ'.2        rw [disjoint_comm] at mJ'        have hs' := moderate_scale_change mJ'.1 hJ mJ'.2        calc          _ ≤ (D : ℝ) ^ s J' / 4 + (8 * D ^ s J' + 8 * D ^ s J) := by            gcongr; exact (dist_lt_of_not_disjoint_ball mJ'.2).le          _ ≤ (D : ℝ) ^ (s J + 1) / 4 + (8 * D ^ (s J + 1) + (8 * D / 25) * D ^ s J) := by            have : (8 : ℝ) ≤ 8 * D / 25 := by              rw [le_div_iff₀ (by norm_num)]; gcongr; exact twentyfive_le_realD X            gcongr; exacts [one_le_realD a, by lia, one_le_realD a, by lia]          _ ≤ _ := by            rw [show 8 * (D : ℝ) / 25 * D ^ s J = 8 / 25 * (D ^ s J * D) by ring,              ← zpow_add_one₀ (by simp), ← add_mul, div_eq_inv_mul, ← add_mul]            gcongr; norm_num  have vpos : 0 < volume (ball (c J) (9 * D ^ (s J + 1))) := by    apply measure_ball_pos volume; unfold defaultD; positivity  rw [ENNReal.mul_le_mul_iff_left vpos.ne' measure_ball_lt_top.ne] at dbl  exact_mod_cast dbl