lean_workbook_plus_33919

Proved

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

Consider the number $A = 10x + a$ with $10^{n - 1} > x\geq 10^{n - 2}$ ( $A$ has $n$ digits) and $a\in\{0,1,2,3,4,5,6,7,8,9\}$ We want to have $a10^{n - 1} + x = 9(10x + a)$ and so $89x = a(10^{n - 1} - 9)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_33919 (n x a : ℕ) (h₁ : 10^(n-1) > x ∧ x ≥ 10^(n-2)) (h₂ : a ∈ Finset.range 10) (h₃ : a*10^(n-1) + x = 9*(10*x + a)) : 89*x = a*(10^(n-1) - 9)   :=  by sorry

Source

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

View graph