Conditional probability and independence

Two fair dice are rolled and you are told that the total is $9$. What is the probability that the first die shows a $5$?

In the lesson's survey of $400$ students in Hanoi, $200$ cycle to school, $80$ were late at least once, and $30$ cyclists were late. A student is chosen at random from those who were late. What is the probability that they cycle?

A condition affects $2\%$ of a population of $10\,000$ people. A test detects it in $90\%$ of people who have it, and gives a false positive for $10\%$ of people who do not. If everyone is tested, how many positive results are expected?

With the numbers of the previous exercise (base rate $2\%$, $90\%$ detection, $10\%$ false positives), a randomly chosen person tests positive. About how likely is it that they have the condition?

Two fair dice are rolled. Which pairs of events are independent? (Choose all that apply.)

Events $A$ and $B$ are mutually exclusive, with $P(A) = 0.3$ and $P(B) = 0.4$. Which statement is true?

Two cards are drawn from a shuffled pack of $52$ without replacement. The probability that both are aces is $\dfrac{1}{N}$. What is $N$?

Here is the proof that if $A$ and $B$ are independent then so are $A$ and $B^c$:

$P(A \cap B^c) \overset{(1)}{=} P(A) - P(A \cap B) \overset{(2)}{=} P(A) - P(A)P(B) \overset{(3)}{=} P(A)\big(1 - P(B)\big) \overset{(4)}{=} P(A)P(B^c)$.

Which step uses the hypothesis that $A$ and $B$ are independent?

In the lesson's Lean model, μ.cond A B is defined as μ.P (A ∩ B) / μ.P B, and Lean's convention makes x / 0 = 0. The lesson proves

theorem bayes (μ : FinProb Ω) (A B : Finset Ω) (hA : μ.P A ≠ 0) : μ.cond A B = μ.cond B A * μ.P A / μ.P B.

What is the role of the hypothesis hA?

Write posterior(prior, sensitivity, false_positive_rate) returning $P(D \mid \text{positive})$ by Bayes' theorem, and after_positives(prior, sensitivity, false_positive_rate, k) returning the probability of $D$ after $k$ positive results from independent tests (use each posterior as the next prior). The tests pass Fractions, so keep the arithmetic exact.