got a little further.. maybe

emily-chandran · emily-chandran · commit f1255fd8ffda · 2025-11-25T11:17:58.000-05:00
diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
@@ -36,6 +36,7 @@ theorem VaR_monotone (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ)
       · have hX : X ω ≤ t := by exact h1 hY
         simp [𝕀, indicator, FinRV.leq, hY, hX]
       · simp [𝕀, indicator, FinRV.leq, hY]
+    simp [cdf]
 
     sorry
   sorry
