lean_workbook_plus_11085

Proved

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

$\frac{\frac{2}{3}\cdot 10}{8}=\frac{\frac{1}{2}\cdot 5}{x}$ ...then $x=3$ . $\boxed{C}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11085  (x : ℝ)
  (h₀ : 2 / 3 * 10 / 8 = 1 / 2 * 5 / x) :
  x = 3   :=  by sorry

Source