Antichain.local_antichain_density

lemma local_antichain_density {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) 𝔄) (ϑ : Θ X) (N : ℕ)    {p' : 𝔓 X} (hp' : ϑ ∈ ball_(p') (𝒬 p') (2 ^ (N + 1))) :    ∑ p ∈ 𝔄_aux 𝔄 ϑ N with 𝔰 p' < 𝔰 p, volume (E p ∩ G ∩ 𝓘 p') ≤      volume (E₂ (2 ^ (N + 3)) p') := by  rw [← MeasureTheory.measure_biUnion_finset _    (fun _ _ ↦  MeasurableSet.inter (measurableSet_E.inter measurableSet_G) coeGrid_measurable)]  · apply measure_mono    simp only [Finset.mem_filter, iUnion_subset_iff, and_imp]    intro p hp hs    by_cases h𝓘 : ((𝓘 p' : Set X) ∩ ↑(𝓘 p)).Nonempty    · exact Ep_inter_G_inter_Ip'_subset_E2 ϑ N hp hp' hs h𝓘    · rw [not_nonempty_iff_eq_empty] at h𝓘      have hemp : (𝓘 p' : Set X) ∩ E p = ∅ :=        eq_empty_of_subset_empty (h𝓘 ▸ inter_subset_inter_right _          (sep_subset ↑(𝓘 p) fun x ↦ Q x ∈ Ω p ∧ 𝔰 p ∈ Icc (σ₁ x) (σ₂ x)))      rw [inter_comm, ← inter_assoc, hemp, empty_inter]      exact empty_subset _  · simp only [Finset.coe_filter]    intro q hq q' hq' hqq'    rw [𝔄_aux, mem_setOf, toFinset_setOf, Finset.mem_filter_univ] at hq hq'    have hE : Disjoint (E q) (E q') := by simpa using (tile_disjointness h𝔄 hq.1.1 hq'.1.1).mt hqq'    rw [Function.onFun, inter_assoc, inter_assoc]    exact (hE.inter_right _).inter_left _