Recovering a proportional quantity

Proved

WorkbookSource.problem_21933

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

lean-workbooksource-checked

$x = ay$ so, when $x = 4$ and $y = 8$ , we have $a = \frac{1}{2}$ Therefore $x = \frac{y}{2}$ and so when $y = 10$ , we get $x = 5$ .

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_21933  (x y a : ℝ)
  (h₀ : x = a * y)
  (h₁ : 4 = a * 8)
  (h₂ : y = 10) :
  x = 5  :=  by sorry

Source

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

View graph