Pr le Pr of implies

theorem Pr_le_Pr_of_implies {α : Type} (D : PMF α)    (f g : α → Prop)    (h_imp : ∀ r, f r → g r) :    Pr_{ let r ← D }[ f r ] ≤ Pr_{ let r ← D }[ g r ] := by  classical  -- 1. Unroll both probability statements into their sum forms  rw [prob_tsum_form_singleton D f]  rw [prob_tsum_form_singleton D g]  -- Goal: ⊢ (∑' r, D r * if f r then 1 else 0) ≤ (∑' r, D r * if g r then 1 else 0)  -- 2. Apply tsum_le_tsum: We need to show term-wise inequality  apply ENNReal.tsum_le_tsum  -- 3. Show the term-wise inequality for each r  intro r  -- Goal: ⊢ D r * (if f r then 1 else 0) ≤ D r * (if g r then 1 else 0)  -- Use `mul_le_mul_left'` which requires proving D r ≠ 0 and D r ≠ ∞  -- Or simpler: use `mul_le_mul_of_nonneg_left` which only requires D r ≥ 0  apply mul_le_mul_of_nonneg_left  -- 4. Prove the inequality between the `ite` terms using the implication  · by_cases hf : f r    · simp only [hf, ↓reduceIte, h_imp, le_refl]    · simp only [hf, ↓reduceIte, zero_le]  -- 5. Prove the factor `D r` is non-negative  · exact zero_le