TileStructure.Forest.approxOnCube_apply

lemma approxOnCube_apply {C : Set (Grid X)} (hC : C.PairwiseDisjoint (fun I ↦ (I : Set X)))    (f : X → E') {x : X} {J : Grid X} (hJ : J ∈ C) (xJ : x ∈ J) :    (approxOnCube C f) x = ⨍ y in J, f y := by  rw [approxOnCube, ← Finset.sum_filter_not_add_sum_filter _ (J = ·)]  have eq0 : ∑ i ∈ Finset.filter (¬ J = ·) (Finset.univ.filter (· ∈ C)),      (i : Set X).indicator (fun _ ↦ ⨍ y in i, f y) x = 0 := by    suffices ∀ i ∈ (Finset.univ.filter (· ∈ C)).filter (¬ J = ·),      (i : Set X).indicator (fun _ ↦ ⨍ y in i, f y) x = 0 by exact Finset.sum_eq_zero this    intro i hi    rw [Finset.mem_filter, Finset.mem_filter_univ] at hi    apply indicator_of_notMem <|      Set.disjoint_left.mp ((hC.eq_or_disjoint hJ hi.1).resolve_left hi.2) xJ  have eq_ave : ∑ i ∈ (Finset.univ.filter (· ∈ C)).filter (J = ·),      (i : Set X).indicator (fun _ ↦ ⨍ y in i, f y) x = ⨍ y in J, f y := by    suffices (Finset.univ.filter (· ∈ C)).filter (J = ·) = {J} by      rw [this, Finset.sum_singleton, Set.indicator_of_mem xJ]    exact subset_antisymm (fun _ h ↦ Finset.mem_singleton.mpr (Finset.mem_filter.mp h).2.symm)      (fun _ h ↦ Finset.mem_filter.mpr ⟨Finset.mem_filter.mpr ⟨Finset.mem_univ _,        (Finset.mem_singleton.mp h) ▸ hJ⟩, (Finset.mem_singleton.mp h).symm⟩)  rw [eq0, eq_ave, zero_add]