condMultiDist_of_hom

theorem condMultiDist_of_hom {G G' S : Type*} [Fintype S]    [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [Finite G]    [MeasurableSpace G'] [MeasurableSingletonClass G'] [AddCommGroup G'] [Finite G']    [MeasurableSpace S] [MeasurableSingletonClass S]    {ι : G →+ G'} (hι : Function.Injective ⇑ι)    {Ω : Type*} (hΩ : MeasureSpace Ω) [IsProbabilityMeasure (ℙ : Measure Ω)]    {m : ℕ} {X : Fin m → Ω → G} (hX : ∀ i, Measurable (X i))    {Y : Fin m → Ω → S} (hY : ∀ i, Measurable (Y i)) (a : Fin m → S → G') :    D[fun i ω ↦ ι (X i ω) + a i (Y i ω) | Y; fun _ ↦ hΩ] = D[X | Y; fun _ ↦ hΩ] := by  cases nonempty_fintype G  cases nonempty_fintype G'  unfold condMultiDist  apply Finset.sum_congr rfl; intro y _  by_cases h : ∀ i, ℙ ( Y i ⁻¹' {y i}) ≠ 0  · congr; calc      _ =  D[fun i ω ↦ ι (X i ω) + a i (y i) ; fun i ↦ ⟨ℙ[|Y i ⁻¹' {y i}]⟩]  := by        convert multiDist_congr (fun i ↦ ⟨ℙ[|Y i ⁻¹' {y i}]⟩) _        intro i        convert! Filter.EventuallyEq.comp₂ (f := fun ω ↦ Y i ω) (f' := fun ω ↦ y i) (g := id)          (g' := id) _ (fun y' ω ↦ ι (X i ω) + a i y') ae_eq_rfl        apply Filter.Eventually.mono (p := fun ω ↦ ω ∈ Y i ⁻¹' {y i})        · apply ae_cond_mem; measurability        intro ω; simp      _ = _ := by        convert multiDist_of_hom' hι (fun i ↦ ⟨ℙ[|Y i ⁻¹' {y i}]⟩) hX _        intro i; exact cond_isProbabilityMeasure (h i)  simp only [ne_eq, not_forall, Decidable.not_not, mul_eq_mul_left_iff] at h ⊢; right  obtain ⟨i, hi⟩ := h; apply Finset.prod_eq_zero (i:= i) <;> simp [hi, Measure.real]