multiDist_of_perm

lemma multiDist_of_perm {m : ℕ} {Ω : Fin m → Type*}    (hΩ : ∀ i, MeasureSpace (Ω i)) (hΩprob : ∀ i, IsProbabilityMeasure (hΩ i).volume)    (X : ∀ i, Ω i → G) (φ : Equiv.Perm (Fin m)) :    D[fun i ↦ X (φ i); fun i ↦ hΩ (φ i)] = D[X ; hΩ] := by  simp only [multiDist]  congr 1  · apply IdentDistrib.entropy_congr    refine {      aemeasurable_fst := by fun_prop      aemeasurable_snd := by fun_prop      map_eq := ?_    }    let sum := fun x : Fin m → G ↦ ∑ i, x i    let perm := MeasurableEquiv.piCongrLeft (fun _ ↦ G) φ    have perm_apply : ∀ (i : Fin m) (x : Fin m → G), perm x i = x (φ.symm i) := by          intro i x          simp only [perm]          rw [MeasurableEquiv.coe_piCongrLeft, Equiv.piCongrLeft_apply]          simp only [eq_rec_constant]    have invar : sum ∘ perm = sum := by      ext x      rw [comp_apply]      convert Finset.sum_bijective φ.symm φ.symm.bijective ?_ ?_      · simp only [Finset.mem_univ, implies_true]      intro i _      rw [perm_apply i x]    calc      _ = Measure.map (sum ∘ perm) (.pi fun i ↦ .map (X (φ i)) ℙ) := by rw [invar]      _ = Measure.map sum (.map perm (.pi fun i ↦ .map (X (φ i)) ℙ)) := by        rw [Measure.map_map]        · apply Finset.measurable_sum          intro i _          exact measurable_pi_apply i        apply measurable_pi_lambda        intro i        have : (fun x : Fin m → G ↦ perm x i) = (fun x : Fin m → G ↦ x (φ.symm i)) := by          ext x          exact perm_apply i x        rw [this]        exact measurable_pi_apply ((Equiv.symm φ) i)      _ = _ := by        congr        exact (MeasureTheory.measurePreserving_piCongrLeft (fun i ↦ .map (X i) ℙ) φ).map_eq  congr 1  convert Finset.sum_bijective φ (Equiv.bijective φ) ?_ ?_  · simp only [Finset.mem_univ, implies_true]  simp only [Finset.mem_univ, imp_self, implies_true]