lean_workbook_plus_42269

Proved

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

Assuming that an item costs 100 dollars, $100 \cdot (1-0.3) \cdot (1-0.2) = 56$ . We reduced the price by 44 dollars, or 44 percent.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42269  (x : ℝ)
  (h₀ : x = 100)
  (h₁ : (1 - 0.3) * (1 - 0.2) = 0.56) :
  x * (1 - 0.3) * (1 - 0.2) = 56   :=  by sorry

Source