Provede2eui

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-muezxens-double-eq (n : Nat) :
    double n = n + n

Edited through the UI smoke test.

How it was proved

Proved: 28 September 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: propext
Proof: 8 lines of Lean