lean_workbook_plus_66701

Proved

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

$\frac{x}{y} = \frac{2}{5}$ means that ${x} = \frac{2y}{5}$ and plugging into $y = 162 - 2x$ we get $y = 162 - \frac{4y}{5}$ . When you solve for $y$ , you get $\frac{9y}{5} = 162$ . Multiply both sides by $\frac{5}{9}$ and you get $y = 90$ . Plugging into the original equation you get $\frac{x}{90} = \frac{2}{5}$ when you solve for $x$ by cross multiplying and dividing by $5$ yields $x = 5$ . So, $y = \boxed{90}$ and $x = \boxed{36}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66701  (x y : ℝ)
  (h₀ : 0 < x ∧ 0 < y)
  (h₁ : x / y = 2 / 5)
  (h₂ : y = 162 - 2 * x) :
  x = 36 ∧ y = 90   :=  by sorry

Source

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

View graph