tendsto_rho_probabilityMeasure

lemma tendsto_rho_probabilityMeasure {α : Type*} {l : Filter α}    [TopologicalSpace Ω] [BorelSpace Ω] [TopologicalSpace G] [BorelSpace G]    [DiscreteTopology G] {X : Ω → G} (hX : Continuous X) (hA : A.Nonempty)    {μ : α → ProbabilityMeasure Ω} {ν : ProbabilityMeasure Ω} (hμ : Tendsto μ l (𝓝 ν)) :    Tendsto (fun n ↦ ρ[X ; (μ n : Measure Ω) # A]) l (𝓝 (ρ[X ; ν # A])) := by  have J (η : ProbabilityMeasure Ω) :      ρ[X ; η # A] = ρ[(id : G → G) ; η.map hX.aemeasurable # A] := by    apply rho_eq_of_identDistrib    exact ⟨hX.aemeasurable, aemeasurable_id, by simp⟩  simp_rw [J]  have Z := ((rho_continuous hA).tendsto ((ν.map hX.aemeasurable)))  have T : Tendsto (fun n ↦ (μ n).map hX.aemeasurable) l (𝓝 (ν.map hX.aemeasurable)) :=    ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous μ ν hμ hX  apply Z.comp T