lean_workbook_plus_51377

Proved

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

The distance the tuna travels in time $t$ is $t \times 13.5 = d_{1}$ The distance the shark travels in time $t$ is $(t-7)\times15 = d_{2}$ ( I guess it's only true if t is greater than 7) When the shark catches the tuna they both will have traveled the same distance so that $d_{1} = d_{2}$ . So if I equate the two equations I can solve for $t$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_51377 (t : ℝ) (d₁ d₂ : ℝ) (h₁ : d₁ = t * 13.5) (h₂ : d₂ = (t-7) * 15) : d₁ = d₂ ↔ t = 70   :=  by sorry

Source

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

View graph