exists_𝔒_with_le_quotient

lemma exists_𝔒_with_le_quotient :    ∃ b ∈ 𝔒 p' l, 2 ^ (-n : ℤ) < volume (E₁ b) / volume (𝓘 b : Set X) := by  classical  have cO : (𝔒 p' l).card ≤ ⌊2 ^ (4 * a) * l ^ a⌋₊ := card_𝔒 _ hl  have ltq : (2 ^ (4 * a) * l ^ a : ℝ≥0) * 2 ^ (-n : ℤ) <      ∑ p'' ∈ 𝔒 p' l, volume (E₁ p'') / volume (𝓘 p'' : Set X) :=    calc      _ < volume (E₂ l p') / volume (𝓘 p' : Set X) := lt_quotient_rearrange qp'      _ ≤ volume (⋃ p'' ∈ 𝔒 p' l, E₁ p'') / volume (𝓘 p' : Set X) := by        gcongr; simp_rw [E₁, E₂, smul, toTileLike, TileLike.toSet]; intro x mx        have rsub := biUnion_Ω (i := 𝓘 p'); rw [range_subset_iff] at rsub; specialize rsub x        simp_rw [mem_iUnion₂, mem_preimage, mem_singleton_iff, exists_prop] at rsub        obtain ⟨(ps : 𝔓 X), (ips : 𝓘 ps = 𝓘 p'), mps⟩ := rsub; rw [← mem_preimage] at mps        rw [mem_iUnion₂]; refine ⟨ps, ?_, ?_⟩        · simp_rw [𝔒, Finset.mem_filter, Finset.mem_univ, ips, true_and, not_disjoint_iff]          use Q x, mem_preimage.mp mx.2, mem_preimage.mp mps        · exact ⟨⟨ips.symm ▸ mx.1.1, mx.1.2⟩, mps⟩      _ ≤ (∑ p'' ∈ 𝔒 p' l, volume (E₁ p'')) / volume (𝓘 p' : Set X) :=        ENNReal.div_le_div_right (measure_biUnion_finset_le _ _) _      _ = ∑ p'' ∈ 𝔒 p' l, volume (E₁ p'') / volume (𝓘 p' : Set X) := by        simp_rw [ENNReal.div_eq_inv_mul, Finset.mul_sum]      _ = _ := by        refine Finset.sum_congr rfl fun p'' mp'' ↦ ?_        rw [𝔒, Finset.mem_filter] at mp''; rw [mp''.2.1]  by_contra! h  have : ∑ p'' ∈ 𝔒 p' l, volume (E₁ p'') / volume (𝓘 p'' : Set X) ≤      (2 ^ (4 * a) * l ^ a : ℝ≥0) * 2 ^ (-n : ℤ) :=    calc      _ ≤ ∑ _ ∈ 𝔒 p' l, (2 : ℝ≥0∞) ^ (-n : ℤ) := Finset.sum_le_sum h      _ = (𝔒 p' l).card * (2 : ℝ≥0∞) ^ (-n : ℤ) := by rw [Finset.sum_const, nsmul_eq_mul]      _ ≤ _ := by        refine mul_le_mul_left ?_ _        rw [show ((𝔒 p' l).card : ℝ≥0∞) = ((𝔒 p' l).card : ℝ≥0) by simp, ENNReal.coe_le_coe]        rw [← Nat.cast_le (α := ℝ≥0)] at cO        exact cO.trans (Nat.floor_le (by positivity))  exact (ltq.trans_le this).false