lean_workbook_plus_81587
ProvedWe are essentially being asked to compute where is the assertion that the special ( white, black) urn was chosen, and is the assertion that both drawn balls are black. By Bayes' Theorem: It is then fairly easily computed that: , , and so . For this to equal requires . There seemed to be a missing backslash at least in the problem statement--which I corrected in quoting it.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_81587 (n : ℕ) (h₀ : 0 < n) (h₁ : (2:ℝ) / (2 + 3 * n) = 1 / 7) : n = 4 := by sorry
Source