multiDist_of_cast

lemma multiDist_of_cast {m m' : ℕ} (h : m' = m) {Ω : Fin m → Type*}    (hΩ : ∀ i, MeasureSpace (Ω i)) (hΩfin : ∀ i, IsFiniteMeasure (hΩ i).volume)    {G : Type*} [MeasurableFinGroup G] (X : ∀ i, Ω i → G) :    D[fun i ↦ X (i.cast h); fun i ↦ hΩ (i.cast h)] = D[X ; hΩ] := by    unfold multiDist    congr 1    · apply IdentDistrib.entropy_congr      refine {        aemeasurable_fst := by fun_prop        aemeasurable_snd := by fun_prop        map_eq := ?_       }      have : (fun (x: Fin m' → G) ↦ ∑ i, x i) =          (fun (x: Fin m → G) ↦ ∑ i, x i) ∘ (fun (x: Fin m' → G) ↦ x ∘ (Fin.cast h.symm)) := by        ext x; dsimp; symm; apply Function.Bijective.sum_comp (Fin.cast_bijective h.symm)      rw [this, ← Measure.map_map] <;> try fun_prop      congr      exact Measure.pi_map_piCongrLeft (finCongr h) (fun i ↦ Measure.map (X i) ℙ)    congr 1    · rw [h]    convert Finset.sum_bijective _ (Fin.cast_bijective h) ?_ ?_ using 1 <;> simp