lean_workbook_plus_57526

Proved

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

Let my rate be $x$ , and my brother's rate be $y$ . Then, we have the following two equations: \n

\begin{cases}9x+4y=1\\8x+7y=1\end{cases}

Solving this gives $(x,y)=\left(\frac3{31},\frac1{31}\right)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_57526  (x y : ℚ)
  (h₀ : 9 * x + 4 * y = 1)
  (h₁ : 8 * x + 7 * y = 1) :
  x = 3 / 31 ∧ y = 1 / 31   :=  by sorry

Source