/workspace/scratch/d3c8f9dc75d7/project/negative_controls/ImpossibleConditionalPrior.lean:9:4: error: unsolved goals
case left
i : Fin 3
⊢ 0 ≤ (∑ i, restrict (sharpP 0) sharpEvent i)⁻¹ * restrict (sharpP 0) sharpEvent i
/workspace/scratch/d3c8f9dc75d7/project/negative_controls/ImpossibleConditionalPrior.lean:11:4: error: unsolved goals
case right
⊢ ∑ i, (∑ i, restrict (sharpP 0) sharpEvent i)⁻¹ * restrict (sharpP 0) sharpEvent i = 1
