lean_workbook_plus_44892

Disproved

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

$\displaystyle\frac{82}{85} = \displaystyle\frac{x}{100}$ , so $x = \displaystyle\frac{100 \times 82}{85} = \boxed{96.47}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44892  (x : ℝ)
  (h₀ : 82 / 85 = x / 100) :
  x = 96.47   :=  by sorry

Source