Solving a positive square-root equation

Proved

WorkbookSource.problem_24733

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

We let $s$ be the slower boat speed. Then $s+5$ is the faster boats speed. In $2$ hours the slower boat will have gone $2s$ km and in $1$ hours the faster boat will have gone $s+5$ km. We use LoC (Law of Cosines) to find the distance between boats is $\sqrt{(2s)^2+(s+5)^2-2(2s)(s+5)\cos(60^{\circ})}=\sqrt{3s^2+25}$ . Setting $\sqrt{3s^2+25}=10$ gives us $s=5$ km/h.

Source: InternLM Lean-Workbook, record lean_workbook_24733 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_24733  (s : ℝ)
  (h₀ : 0 < s)
  (h₁ : Real.sqrt (3 * s^2 + 25) = 10) :
  s = 5  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_24733; Apache-2.0

View graph