TileStructure.Forest.cntp_approxOnCube_eq

lemma cntp_approxOnCube_eq (hu₁ : u₁ ∈ t) :    approxOnCube (𝓙 (t u₁))      (‖(𝓘 u₁ : Set X).indicator (adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f₂) ·‖) =    approxOnCube (𝓙₆ t u₁) (‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f₂ ·‖) := by  set U := (𝓘 u₁ : Set X)  ext x; simp only [approxOnCube]  classical  calc    _ = ∑ p with p ∈ 𝓙₆ t u₁, (p : Set X).indicator (fun x ↦ ⨍ y in p,        ‖U.indicator (adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f₂) y‖) x := by      apply (Finset.sum_subset (fun p mp ↦ ?_) (fun p mp np ↦ ?_)).symm      · rw [Finset.mem_filter_univ] at mp ⊢        exact mp.1      · rw [Finset.mem_filter_univ] at mp np        rw [indicator_apply_eq_zero]; intro mx        rw [show (0 : ℝ) = ⨍ y in (p : Set X), 0 by simp]        refine setAverage_congr_fun coeGrid_measurable (.of_forall fun y my ↦ ?_)        suffices Disjoint (p : Set X) U by          rw [indicator_of_notMem (this.notMem_of_mem_left my), norm_zero]        -- There has to be a cube `I ∈ 𝓙₆` (the one containing `c (𝓘 u₁)`)        have cm : c (𝓘 u₁) ∈ (𝓘 u₁ : Set X) := Grid.c_mem_Grid        rw [← union_𝓙₆ hu₁, mem_iUnion₂] at cm; obtain ⟨I, mI, hI⟩ := cm        -- Obviously `I ≠ p`        have nIp : I ≠ p := ne_of_mem_of_not_mem mI np        -- If `U` intersected `p`, `U ≤ p` since `p ∉ 𝓙₆`        by_contra! h        rw [𝓙₆, mem_inter_iff, not_and, mem_Iic] at np; specialize np mp        have Ulp := le_or_ge_or_disjoint.resolve_left np |>.resolve_right h        -- `I`, being in `𝓙₆`, should be a maximal cube in `𝓙₀ 𝔖`,        -- but `p` is above it and also in `𝓙₀ 𝔖`; contradiction        rw [𝓙₆, mem_inter_iff, mem_Iic] at mI        rw [𝓙, mem_setOf] at mp mI        exact nIp <| le_antisymm (mI.2.trans Ulp) (mI.1.2 mp.1 (mI.2.trans Ulp))    _ = _ := by      congr! 3 with p mp      refine setAverage_congr_fun coeGrid_measurable (.of_forall fun y my ↦ ?_)      rw [Finset.mem_filter_univ, 𝓙₆, mem_inter_iff, mem_Iic] at mp      rw [indicator_of_mem (mp.2.1 my)]