lean_workbook_plus_46047

Proved

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

Let the height of the trapezoid be $h$ . Then we have $\frac{h}{\sqrt3}+4+h\sqrt3=16$ , so $h=3\sqrt3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46047  (h : ℝ)
  (hh : 0 < h)
  (hh2 : (h / Real.sqrt 3 + 4 + h * Real.sqrt 3) = 16) :
  h = 3 * Real.sqrt 3   :=  by sorry

Source

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

View graph