lean_workbook_plus_64781
ProvedAnother way: Suppose is the expected time. Then is equal to (time if he picks the first opening), plus (time if he picks the second opening; the plus E is because he's at the exact same situation after he traveled 3 hours), plus (time if he picks the third opening, see above). So So he will need 10 hours on average.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64781 (e : ℝ) (h₀ : e = (2 + (3 + e) + (5 + e)) / 3) : e = 10 := by sorry
Source