exists_k_of_mem_𝔓pos

lemma exists_k_of_mem_𝔓pos (h : p ∈ 𝔓pos (X := X)) : ∃ k, p ∈ TilesAt k := by  let C : Set ℕ := {k | 𝓘 p ∈ aux𝓒 k}  have Cn : C.Nonempty := by    rw [𝔓pos, mem_setOf] at h    have vpos : 0 < volume (G ∩ 𝓘 p) := by      rw [inter_comm]; exact h.trans_le (measure_mono inter_subset_left)    obtain ⟨k, hk⟩ := exists_mem_aux𝓒 vpos; exact ⟨_, hk⟩  let s : ℕ := WellFounded.min wellFounded_lt _ Cn  have s_mem : s ∈ C := WellFounded.min_mem ..  have s_min : ∀ t ∈ C, s ≤ t := fun t mt ↦ WellFounded.min_le _ mt  have s_pos : 0 < s := by    by_contra! h; rw [nonpos_iff_eq_zero] at h    simp_rw [h, C, aux𝓒, mem_setOf] at s_mem; apply absurd s_mem; push Not; intro _ _    rw [Int.neg_ofNat_zero, zpow_zero, one_mul]; exact measure_mono inter_subset_right  use s - 1; rw [TilesAt, mem_preimage, 𝓒, mem_sdiff, Nat.sub_add_cancel s_pos]  have : ∀ t < s, t ∉ C := fun t mt ↦ by contrapose! mt; exact s_min t mt  exact ⟨s_mem, this (s - 1) (Nat.sub_one_lt_of_lt s_pos)⟩