proofs
Provednlightninglightningpr-14formal-invariant

Onion replay-set insertion is idempotent

For all α∈Type⁡\htmlData{mx=1}{\alpha \in \htmlData{mx=0}{\operatorname{Type}}}, s∈Finset⁡ α\htmlData{mx=3}{s \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Finset}}\,\htmlData{mx=1}{\alpha}}} and x∈α\htmlData{mx=1}{x \in \htmlData{mx=0}{\alpha}} (given DecidableEq⁡ α\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{DecidableEq}}\,\htmlData{mx=1}{\alpha}}):

insert⁡(x,insert⁡(x,s))=insert⁡(x,s)\htmlData{mx=6}{\htmlData{mx=0}{\operatorname{insert}}(\htmlData{mx=1}{x}, \htmlData{mx=5}{\htmlData{mx=2}{\operatorname{insert}}(\htmlData{mx=3}{x}, \htmlData{mx=4}{s})})} \mathrel{\htmlData{mx=11}{=}} \htmlData{mx=10}{\htmlData{mx=7}{\operatorname{insert}}(\htmlData{mx=8}{x}, \htmlData{mx=9}{s})}
What the notation means · or point at any symbol
Type
Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
DecidableEq
DecidableEq: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (DecidableEq)
f(x)Function application
DecidableEq applied to α. Lean writes f x; papers write f(x). (DecidableEq α)
Finset
Finset: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset)
insert
insert: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (insert)
=Equality
insert(x, insert(x, s)) and insert(x, s) are the same. (insert x (insert x s) = insert x s)

Finite-set model of duplicate replay-key recording.

How it was proved

Proved
6 October 2026
By
Ajax
Checked by
Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms
Classical.choice, Quot.sound, propext
Proof
6 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements