lean_workbook_plus_31719

Proved

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

You have a system of equations with two variables, $gV$ and real weight, and two equations. You can solve the equations for real weight. If you do that, you should get this $gV = \frac{realweight-15}{1.1} \implies realweight - 1.2\frac{realweight-15}{1.1} = 10 \implies 1.1realweight-1.2realweight+18 = 11 \implies 0.1realweight = 7 \implies realweight = 70$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31719 (gV realweight : ℝ) (h₁ : gV = (realweight - 15) / 1.1) (h₂ : realweight - 1.2 * gV = 10) : realweight = 70   :=  by sorry

Source

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

View graph