lean_workbook_plus_20959

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Let the number of apples remaining in the three baskets be $x$ . For the first basket, the number of apples, $x$ , is $\frac56$ of what was originally there. This means there were originally $\frac65x$ apples in that basket. Similarly, the second basket originally had $\frac{13}{10}x$ apples and the third basket originally had $\frac32x$ apples. Therefore, $\frac65x+\frac{13}{10}x+\frac32x=2000\implies x=500$ Hence, the three baskets originally had $\boxed{600,650,750}$ apples respectively.

Why this node was retired

The posted statement is

theorem lean_workbook_plus_20959  (x : ℕ)
  (h₀ : 5 / 6 * x + 13 / 10 * x + 3 / 2 * x = 2000) :
  x = 500   :=  by sorry

The first coefficient was inverted and all coefficients were subjected to natural division.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

For rational or real x, use(6/5)x+(13/10)x+(3/2)x=2000 and conclude x=500; if x counts apples add integrality after preserving rational coefficients.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.