multiDist_of_hom'

theorem multiDist_of_hom' {G G' : Type*} [MeasurableSpace G] [MeasurableSingletonClass G]    [AddCommGroup G] [Finite G] [MeasurableSpace G'] [MeasurableSingletonClass G']    [AddCommGroup G'] [Finite G'] {ι : G →+ G'} (hι : Function.Injective ⇑ι) {m : ℕ}    {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))    [∀ i, IsProbabilityMeasure (ℙ : Measure (Ω i))] {X : ∀ i, Ω i → G} (hX : ∀ i, Measurable (X i))    (a : Fin m → G') : D[fun i ω ↦ ι (X i ω) + a i; hΩ] = D[X; hΩ] := by  unfold multiDist  congr 1  · unfold entropy    set sum_G : (Fin m → G) → G := fun x ↦ ∑ i, x i    set sum_G' : (Fin m → G') → G' := fun x ↦ ∑ i, x i    let ι' : G → G' := fun x ↦ ι x + ∑ i, a i    have hι' : Function.Injective ι' := by simpa [ι', Injective]    convert measureEntropy_map_of_injective _ ι' _ hι' <;> try fun_prop    rw [Measure.map_map] <;> try fun_prop    have : ι' ∘ sum_G = sum_G' ∘ (fun x i ↦ ι (x i) + a i) := by      ext x; simp [ι', sum_G, sum_G', Finset.sum_add_distrib]    rw [this, ←Measure.map_map] <;> try fun_prop    congr    convert (Measure.map_of_pi (f := fun i x ↦ ι x + a i) _ _).symm with i    · rw [Measure.map_map] <;> try fun_prop      congr    · intro i; exact isProbabilityMeasure_map (by fun_prop)    intro i; fun_prop  congr 2; ext i  apply entropy_comp_of_injective _ (hX i) (fun x ↦ ι x + a i) _  intro x y hxy; simp only [_root_.add_left_inj] at hxy; exact hι hxy