continuous_rdist_restrict_probabilityMeasure

lemma continuous_rdist_restrict_probabilityMeasure [Finite G]    [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G] :    Continuous      (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦        d[id ; μ.1.toMeasure # id ; μ.2.toMeasure]) := by  simp [rdist_def]  have obs₀ : Continuous (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦      H[fun x ↦ x.1 - x.2 ; μ.1.toMeasure.prod μ.2.toMeasure]) := by    simp_rw [entropy_def]    have diff_cts : Continuous (fun (x : G × G) ↦ x.1 - x.2) := by continuity    have key₁ := ProbabilityMeasure.continuous_prod (α := G) (β := G)    have key₂ := ProbabilityMeasure.continuous_map diff_cts    convert! continuous_measureEntropy_probabilityMeasure.comp (key₂.comp key₁)  have obs₁ : Continuous      (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦ H[id ; μ.1.toMeasure]) := by    convert (continuous_measureEntropy_probabilityMeasure (Ω := G)).comp continuous_fst    simp [entropy_def]  have obs₂ : Continuous      (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦ H[id ; μ.2.toMeasure]) := by    convert (continuous_measureEntropy_probabilityMeasure (Ω := G)).comp continuous_snd    simp [entropy_def]  continuity