lean_workbook_plus_5034
ProvedSubstituting into the first known equation, we can solve for : \n \begin{align*}\frac{3b}{5}+b&=24\ 3b+5b&=120\ b&=15\end{align*}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5034 (a b : ℝ) (h₁ : a + b = 24) (h₂ : a = 3 * b / 5) : b = 15 := by sorry
Source