condMultiDist_of_const

theorem condMultiDist_of_const {G : Type*} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ}    {Ω : Fin m → Type*} [hΩ : ∀ i, MeasureSpace (Ω i)] [∀ i, IsProbabilityMeasure (hΩ i).volume]    {S : Type*} [Fintype S] (c : Fin m → S) (X : ∀ i, Ω i → G) :    D[X | fun i ↦ fun _ ↦ c i; hΩ] = D[X ; hΩ] := by  dsimp [condMultiDist]  rw [Finset.sum_eq_single c]  · have : ∀ i, (fun _:Ω i ↦ c i) ⁻¹' {c i} = Set.univ := by      intros; simp only [Set.mem_singleton_iff, Set.preimage_const_of_mem]    simp [this]  · intro y _ hy    convert zero_mul _    contrapose! hy    rw [Finset.prod_ne_zero_iff] at hy    ext i    replace hy := hy i (Finset.mem_univ i)    contrapose! hy    have : (fun _:Ω i ↦ c i) ⁻¹' {y i} = ∅ := by      ext ω      simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_empty_iff_false, iff_false]      exact id (Ne.symm hy)    simp [this]  simp only [Finset.mem_univ, not_true_eq_false, false_implies]