condRho_eq_of_identDistrib

lemma condRho_eq_of_identDistrib {S : Type*} [MeasurableSpace S] [MeasurableSingletonClass S]    {Y : Ω → G} {W : Ω → S} {Ω' : Type*} [MeasurableSpace Ω'] {μ' : Measure Ω'}    {Y' : Ω' → G} {W' : Ω' → S} (hY : Measurable Y) (hW : Measurable W) (hY' : Measurable Y')    (hW' : Measurable W')    (h : IdentDistrib (⟨Y, W⟩) (⟨Y', W'⟩) μ μ') :    ρ[Y | W ; μ # A] = ρ[Y' | W' ; μ' # A] := by  rw [condRho]  congr with g  have M : μ (W ⁻¹' {g}) = μ' (W' ⁻¹' {g}) := by    have I : IdentDistrib W W' μ μ' := h.comp (u := Prod.snd) measurable_snd    rw [← map_apply hW (.singleton _), ← map_apply hW' (.singleton _), I.map_eq]  have M' : μ.real (W ⁻¹' {g}) = μ'.real (W' ⁻¹' {g}) := by simp [measureReal_def, M]  rw [M']  congr 1  apply rho_eq_of_identDistrib  refine ⟨hY.aemeasurable, hY'.aemeasurable, ?_⟩  ext s hs  rw [map_apply hY hs, map_apply hY' hs, cond_apply (hW (.singleton _)),    cond_apply (hW' (.singleton _)), M]  congr  have E : W ⁻¹' {g} ∩ Y ⁻¹' s = (⟨Y, W⟩) ⁻¹' (s ×ˢ {g}) := by ext; aesop  have F : W' ⁻¹' {g} ∩ Y' ⁻¹' s = (⟨Y', W'⟩) ⁻¹' (s ×ˢ {g}) := by ext; aesop  rw [E, F, ← map_apply (by fun_prop) (hs.prod (.singleton _)),    ← map_apply (by fun_prop) (hs.prod (.singleton _)), h.map_eq]