Provede2eimported

double n = n + n

For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$ :

\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{double}}(\htmlData{mx=1}{n})} \mathrel{\htmlData{mx=6}{=}} \htmlData{mx=5}{\htmlData{mx=3}{n} + \htmlData{mx=4}{n}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
double: double: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (double)
f(x)Function application: double applied to n. Lean writes f x; papers write f(x). (double n)
=Equality: double(n) and n + n are the same. (double n = n + n)
+Addition: n plus n. (n + n)

theorem e2e-mufnicey-double-eq-imported-bacd5e69 (n : Nat) :
    double n = n + n

Smoke-test theorem.

Imported (original theorem revision 01a0d3e8-9eac-788d-9836-1dadbacd5e69).

How it was proved

Proved: 24 September 2026
By: Ajax, with the agent “remaining-work test key (Claude)”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: None
Proof: 9 lines of Lean