TileStructure.Forest.lintegral_eq_lintegral_approxOnCube

lemma lintegral_eq_lintegral_approxOnCube {C : Set (Grid X)}    (hC : C.PairwiseDisjoint fun I ↦ (I : Set X)) {J : Grid X} (hJ : J ∈ C) {f : X → ℂ}    (hf : BoundedCompactSupport f) :    ∫⁻ y in J, ‖f y‖ₑ = ∫⁻ y in J, ‖approxOnCube C (fun x ↦ (‖f x‖ : ℂ)) y‖ₑ := by  have nonneg : 0 ≤ᶠ[ae (volume.restrict J)] fun y ↦ ‖f y‖ := Filter.Eventually.of_forall (by simp)  have vol_J_ne_zero := (volume_coeGrid_pos (X := X) (i := J) (defaultD_pos a)).ne.symm  have eq : ∫⁻ y in J, ‖approxOnCube C (fun x ↦ (‖f x‖ : ℂ)) y‖ₑ =      ∫⁻ y in (J : Set X), ENNReal.ofReal (⨍ z in J, ‖f z‖) := by    refine setLIntegral_congr_fun coeGrid_measurable fun y hy ↦ ?_    rw [approxOnCube_apply hC _ hJ hy, ← ofReal_norm]    apply congrArg    have : ‖⨍ y in J, (‖f y‖ : ℂ)‖ = ‖⨍ y in J, ‖f y‖‖ := by      convert! congrArg (‖·‖) <| integral_ofReal (f := (‖f ·‖)) using 1      simp [average]    rw [this, Real.norm_eq_abs, abs_eq_self]    apply integral_nonneg (fun y ↦ by simp)  rw [eq, lintegral_const, average_eq, smul_eq_mul, ENNReal.ofReal_mul, ENNReal.ofReal_inv_of_pos,    ofReal_integral_eq_lintegral_ofReal hf.norm.integrable.restrict nonneg, mul_comm,    ← mul_assoc, Measure.restrict_apply MeasurableSet.univ, univ_inter]  · simp only [Measure.real,      Measure.restrict_apply_univ,      ENNReal.ofReal_toReal volume_coeGrid_lt_top.ne,      ENNReal.mul_inv_cancel vol_J_ne_zero volume_coeGrid_lt_top.ne,      one_mul,      ofReal_norm    ]  · simpa using! ENNReal.toReal_pos vol_J_ne_zero volume_coeGrid_lt_top.ne  · exact inv_nonneg.mpr ENNReal.toReal_nonneg