Tv Dist bind left le const

theorem tvDist_bind_left_le_const    {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF]    [MonadLiftT m SetM] [EvalDistCompatible m]    {α β : Type u} (mx : m α) (f g : α → m β) (c : ℝ)    (hfg : ∀ a, a ∈ support mx → tvDist (f a) (g a) ≤ c) :    tvDist (mx >>= f) (mx >>= g) ≤ c := by  classical  have hprob_ne_top : ∀ a : α, Pr[= a | mx] ≠ ⊤ := fun a =>    ne_top_of_le_ne_top one_ne_top (probOutput_le_one (mx := mx) (x := a))  have hp_sum_ne_top : (∑' a : α, Pr[= a | mx]) ≠ ⊤ := by    rw [tsum_probOutput_of_liftM_PMF]; exact one_ne_top  have hp_summable : Summable (fun a : α => Pr[= a | mx].toReal) :=    ENNReal.summable_toReal hp_sum_ne_top  have hp_sum_toReal : (∑' a : α, Pr[= a | mx].toReal) = 1 := by    rw [← ENNReal.tsum_toReal_eq hprob_ne_top, tsum_probOutput_of_liftM_PMF, ENNReal.toReal_one]  have hlhs_nonneg : ∀ a : α, 0 ≤ Pr[= a | mx].toReal * tvDist (f a) (g a) :=    fun _ => mul_nonneg ENNReal.toReal_nonneg (tvDist_nonneg _ _)  have hlhs_le_p : ∀ a : α,      Pr[= a | mx].toReal * tvDist (f a) (g a) ≤ Pr[= a | mx].toReal :=    fun _ => mul_le_of_le_one_right ENNReal.toReal_nonneg (tvDist_le_one _ _)  have hlhs_summable :      Summable (fun a : α => Pr[= a | mx].toReal * tvDist (f a) (g a)) :=    Summable.of_nonneg_of_le hlhs_nonneg hlhs_le_p hp_summable  have hrhs_summable : Summable (fun a : α => Pr[= a | mx].toReal * c) :=    Summable.mul_right _ hp_summable  refine (tvDist_bind_left_le mx f g).trans ?_  calc    (∑' a : α, Pr[= a | mx].toReal * tvDist (f a) (g a))        ≤ ∑' a : α, Pr[= a | mx].toReal * c :=          Summable.tsum_le_tsum            (fun a => by              by_cases ha : a ∈ support mx              · exact mul_le_mul_of_nonneg_left (hfg a ha) ENNReal.toReal_nonneg              · rw [probOutput_eq_zero_of_not_mem_support ha]; simp)            hlhs_summable hrhs_summable    _ = (∑' a : α, Pr[= a | mx].toReal) * c := Summable.tsum_mul_right _ hp_summable    _ = c := by rw [hp_sum_toReal, one_mul]