English
If a ∉ s, then insert a s = insert b s implies a = b.
Русский
Если a ∉ s, то insert a s = insert b s подразумевает a = b.
LaTeX
$$$\bigl(a \notin s\bigr) \Rightarrow \bigl(\operatorname{insert}(a,s) = \operatorname{insert}(b,s) \iff a = b\bigr)$$$
Lean4
theorem insert_inj (ha : a ∉ s) : insert a s = insert b s ↔ a = b :=
⟨fun h => eq_of_mem_insert_of_notMem (h ▸ mem_insert a s) ha, congr_arg (fun x => insert x s)⟩