lean_workbook_plus_30983

Proved

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

If $a = b = 2c$ and $abc = 864$ , then the value of $a + b + c$ is equal: \n\n a) 16 \n b) 23 \n c) 30 \n d) 32 \n e) 34

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30983 (a b c : ℝ) (h₁ : a = b ∧ b = 2*c) (h₂ : a*b*c = 864) : a + b + c = 30   :=  by sorry

Source