lean_workbook_plus_5464

Proved

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

Ok, the original volume is $150000cm^{3}$ from multiplying the dimensions $100*30*50$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5464 (l₁ l₂ l₃ : ℝ) (h₁ : l₁ = 100) (h₂ : l₂ = 30) (h₃ : l₃ = 50) : l₁ * l₂ * l₃ = 150000   :=  by sorry

Source