TileStructure.Forest.adjoint_tile_support1

lemma adjoint_tile_support1 : adjointCarleson p f =    (ball (𝔠 p) (5 * D ^ 𝔰 p)).indicator (adjointCarleson p ((𝓘 p : Set X).indicator f)) := by  rw [adjoint_eq_adjoint_indicator E_subset_𝓘]; ext x  rcases eq_or_ne (adjointCarleson p ((𝓘 p : Set X).indicator f) x) 0 with h0 | hn  · exact (indicator_apply_eq_self.mpr fun _ ↦ h0).symm  refine (indicator_of_mem ?_ _).symm  obtain ⟨y, my, Ky⟩ : ∃ y ∈ 𝓘 p, Ks (𝔰 p) y x ≠ 0 := by    contrapose! hn    refine setIntegral_eq_zero_of_forall_eq_zero fun y my ↦ ?_    simp only [defaultA, mul_eq_zero, map_eq_zero, exp_ne_zero,      or_false, indicator_apply_eq_zero]    left    exact hn _ (E_subset_𝓘 my)  rw [mem_ball]  calc    _ ≤ dist y x + dist y (𝔠 p) := dist_triangle_left ..    _ < D ^ 𝔰 p / 2 + 4 * (D : ℝ) ^ 𝔰 p :=      add_lt_add_of_le_of_lt (dist_mem_Icc_of_Ks_ne_zero Ky).2 (mem_ball.mpr (Grid_subset_ball my))    _ ≤ _ := by rw [div_eq_mul_inv, mul_comm, ← add_mul]; gcongr; norm_num