lean_workbook_plus_50876
ProvedFrom the first condition and the symmetry that it creates, we know that the probability of getting heads on the first coin is the same as the probability of getting tails on the second coin. Let this probability be . Also, the probability of getting tails on the first coin is the same as the probability of getting heads on the second coin. Let this probability be .\n\nFrom the second condition, we know that . This leads to , which leads to . Since we don't really know which coin is which, this actually makes perfect sense...especially the fact that the probabilities sum to .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_50876 (p : ℝ) (h₀ : 0 ≤ p ∧ p ≤ 1) (h₁ : (p^2) + ((1 - p)^2) = 5 / 8) : p = 1 / 4 ∨ p = 3 / 4 := by sorry
Source