lean_workbook_plus_41352

Proved

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

Using proportions, we get that $\frac{4}{15}=\frac{x}{60}$ , where $x$ is the number of bass that C.A can catch in an hour. This comes out to $15x=4\times60$ , which simplifies to $15x=240$ . Divide by 15 to get $x=16$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_41352  (x : ℝ)
  (h₀ : 0 < x)
  (h₁ : 15 / 4 = 60 / x) :
  x = 16   :=  by sorry

Source

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

View graph