lean_workbook_plus_50224

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

So the fraction of the distance with Ann on horseback is $\frac{17.9vt}{17.9vt+\dfrac{3124vt}{629}}=\boxed{\frac{112591}{143831}}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50224  (v t : ℝ)
  (h₀ : 0 < v ∧ 0 < t)
  (h₁ : 3124 * v * t / 629 + 17.9 * v * t = 1) :
  17.9 * v * t / (17.9 * v * t + 3124 * v * t / 629) = 112591 / 143831   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph