lean_workbook_plus_71799

Proved

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

Let $a$ be the distance between him and his house, and $b$ be the distance between him and the stadium. \n\n $b=a+\frac{a+b}7$ \n\n $7b=7a+a+b$ \n\n $6b=8a$ \n\n $\frac{a}b=\frac34\Rightarrow\boxed{\text{C}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71799  (a b : ℝ)
  (h₀ : 0 < a ∧ 0 < b)
  (h₁ : b = a + (a + b) / 7) :
  a / b = 3 / 4   :=  by sorry

Source

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

View graph