exists_mem_aux𝓒

lemma exists_mem_aux𝓒 {i : Grid X} (hi : 0 < volume (G ∩ i)) : ∃ k, i ∈ aux𝓒 (k + 1) := by  have vlt : volume (i : Set X) < ⊤ := volume_coeGrid_lt_top  have one_le_quot : 1 ≤ volume (i : Set X) / volume (G ∩ i) := by    rw [ENNReal.le_div_iff_mul_le (Or.inl hi.ne') (Or.inr vlt.ne), one_mul]    exact measure_mono inter_subset_right  have quot_ne_top : volume (i : Set X) / volume (G ∩ i) ≠ ⊤ := by    rw [Ne, ENNReal.div_eq_top, not_or, not_and_or, not_and_or]    exact ⟨Or.inr hi.ne', Or.inl vlt.ne⟩  have ornz : 0 < (volume (i : Set X) / volume (G ∩ i)).toReal :=    ENNReal.toReal_pos (zero_lt_one.trans_le one_le_quot).ne' quot_ne_top  let k : ℝ := Real.logb 2 (volume (i : Set X) / volume (G ∩ i)).toReal  use ⌊k⌋₊, i, le_rfl  nth_rw 1 [← ENNReal.mul_lt_mul_iff_right (show 2 ^ (⌊k⌋₊ + 1) ≠ 0 by simp) (by simp), ← mul_assoc,    ← ENNReal.rpow_natCast, ← ENNReal.rpow_intCast, ← ENNReal.rpow_add _ _ (by simp) (by simp)]  rw [Int.cast_neg, Int.cast_natCast, add_neg_cancel, ENNReal.rpow_zero, one_mul,    ← ENNReal.div_lt_iff (Or.inl hi.ne') (Or.inr vlt.ne), ← ENNReal.ofReal_toReal quot_ne_top,    ← @ENNReal.ofReal_toReal (2 ^ (⌊k⌋₊ + 1)) (by simp), ENNReal.ofReal_lt_ofReal_iff (by simp),    ENNReal.toReal_pow, ENNReal.toReal_ofNat, ← Real.rpow_natCast,    ← Real.logb_lt_iff_lt_rpow one_lt_two ornz]  exact Nat.lt_succ_floor k