lean_workbook_plus_56997

Proved

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

The actual length of the diagonal, which we will call x, is \n $\frac {\frac {3}{2}}{400}=\frac {\frac {3}{16}}{x}$ . This simplifies out to $x=50$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_56997  (x : ℝ)
  (h₀ : 0 < x)
  (h₁ : (3 / 2) / 400 = (3 / 16) / x) :
  x = 50   :=  by sorry

Source