lean_workbook_plus_42806
ProvedLet, be the probability that the first archer wins. Take the first aim. The first archer wins on that aim with probability and with probability the game continues to the second shot. The moment that happens, it's just as if we were starting over, except that the roles are now reversed - and the first archer's overall winning probability, given that he didn't win on the first shot, is So
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_42806 (p : ℝ) (h₀ : p = 1 / 2 + 1 / 2 * (1 - p)) : p = 2 / 3 := by sorry
Source