TileStructure.Forest.sum_p_eq_sum_I_sum_p

lemma sum_p_eq_sum_I_sum_p (f : X → ℤ → ℝ≥0∞) :    ∑ p ∈ Finset.univ.filter (· ∈ t u), (E p).indicator 1 x * f (𝔠 p) (𝔰 p) =    ∑ I : Grid X, ∑ p ∈ Finset.univ.filter (fun p ↦ p ∈ t u ∧ 𝓘 p = I),    (E p).indicator 1 x * f (c I) (s I) := by  set ps := fun (I : Grid X) ↦ Finset.univ.filter (fun p ↦ p ∈ t u ∧ 𝓘 p = I)  calc  _ = ∑ p ∈ Finset.univ.biUnion ps, (E p).indicator 1 x * f (𝔠 p) (𝔰 p) :=    have hps_eq : Finset.univ.filter (· ∈ t u) = Finset.univ.biUnion ps := by      ext p      simp only [ps, Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_biUnion,        exists_and_left]      exact ⟨fun h ↦ ⟨h, _, rfl⟩, And.left⟩    Finset.sum_congr hps_eq (fun _ _ ↦ rfl)  _ = ∑ I : Grid X, ∑ p ∈ Finset.univ.filter (fun p ↦ p ∈ t u ∧ 𝓘 p = I),        (E p).indicator 1 x * f (𝔠 p) (𝔰 p) := by    refine (Finset.sum_biUnion ?_)    intro I _ J _ I_ne_J a haI haJ p hp    apply False.elim ∘ I_ne_J    specialize haI hp    specialize haJ hp    simp only [mem_𝔗, ps, Finset.mem_filter] at haI haJ    rw [← haI.2.2, ← haJ.2.2]  _ = _ := by    refine Finset.sum_congr rfl (fun I _ ↦ Finset.sum_congr rfl (fun p hp ↦ ?_))    rw [← (Finset.mem_filter.mp hp).2.2, 𝔰, 𝔠]