lean_workbook_plus_48646
ProvedLet the speed of the train be .\nLet the distance be .\nLet the original time be .\nIf the train hadn't broken down, then ...........(1)\nBut when the train suffers a breakdown.\nThen\n \nSo, ...........(2) (Because for the first 1.5 hrs it travels with speed , then 0.5 hrs for repairs, this gives hrs in which it travels at speed ).\n\nCombining equation (1) and (2) and solving, we get\n .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48646 (v d t : ℝ) (h₀ : 0 < v ∧ 0 < d ∧ 0 < t) (h₁ : v * t = d) (h₂ : 3 / 2 * v + 4 / 5 * v * (t + 1) = d) : d / v = 23 / 2 := by sorry
Source