exists_j_of_mem_𝔓pos_ℭ

lemma exists_j_of_mem_𝔓pos_ℭ (h : p ∈ 𝔓pos (X := X)) (mp : p ∈ ℭ k n) (hkn : k ≤ n) :    p ∈ 𝔏₀ k n ∨ ∃ j ≤ 2 * n + 3, p ∈ ℭ₁ k n j := by  classical  rw [𝔓pos, mem_setOf, inter_comm _ G'ᶜ, ← inter_assoc] at h  replace h : 0 < volume (G'ᶜ ∩ (𝓘 p : Set X)) := h.trans_le (measure_mono inter_subset_left)  rw [inter_comm, G', compl_union, compl_union, inter_comm G₁ᶜ, ← inter_assoc, ← inter_assoc] at h  replace h : 0 < volume ((𝓘 p : Set X) ∩ G₂ᶜ) :=    h.trans_le (measure_mono (inter_subset_left.trans inter_subset_left))  obtain ⟨x, mx, nx⟩ := nonempty_of_measure_ne_zero h.ne'  simp_rw [G₂, mem_compl_iff, mem_iUnion] at nx; push Not at nx; specialize nx n k hkn  let B : ℕ := Finset.card { q | q ∈ 𝔅 k n p }  have Blt : B < 2 ^ (2 * n + 4) := by    calc      _ ≤ Finset.card { m | m ∈ 𝔐 k n ∧ x ∈ 𝓘 m } := by        apply Finset.card_le_card (Finset.monotone_filter_right _ ?_)        refine fun a _ha ha' ↦ ⟨mem_of_mem_inter_left ha', ?_⟩        obtain ⟨m₁, m₂⟩ := ha'        exact m₂.1.1 mx      _ = stackSize (𝔐 k n) x := by        simp_rw [stackSize, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id,          Finset.filter_filter]; rfl      _ ≤ (2 * n + 6) * 2 ^ (n + 1) := by rwa [setA, mem_setOf, not_lt] at nx      _ < _ := by        rw [show 2 * n + 4 = (n + 3) + (n + 1) by lia, pow_add _ (n + 3)]        exact mul_lt_mul_of_pos_right two_mul_n_add_six_lt (by positivity)  rcases B.eq_zero_or_pos with Bz | Bpos  · simp_rw [B, filter_mem_univ_eq_toFinset, Finset.card_eq_zero, toFinset_eq_empty] at Bz    exact Or.inl ⟨mp, Bz⟩  · right; use Nat.log 2 B; rw [← Nat.log_lt_iff_lt_pow one_lt_two Bpos.ne'] at Blt    refine ⟨by lia, (?_ : _ ∧ _ ≤ B), (?_ : ¬(_ ∧ _ ≤ B))⟩    · exact ⟨mp, Nat.pow_log_le_self 2 Bpos.ne'⟩    · rw [not_and, not_le]; exact fun _ ↦ Nat.lt_pow_succ_log_self one_lt_two _