1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36

import Mathlib
import Lean

variable [LinearOrder α] (xs : List α)

def ins (a : α)
  | [] => [a]
  | x :: xs =>
    if a ≤ x then a :: x :: xs else x :: ins a xs

def List.insSort : List α → List α
  | [] => []
  | x :: xs => ins x xs.insSort

def Sorted : List α → Prop
  | [] | [_] => True
  | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs)

open Lean Environment

def emptDecl : Declaration :=
  .thmDecl { name := `empt
             levelParams := []
             type := .const ``Empty []
             value := .lit (.strVal "😈") }

elab "add_empt" : command => do
  let env' := addDeclCore (← get).env 0 emptDecl none 0
  match env' with
  | .error _ => throwError "@"
  | .ok e => modifyEnv (fun _ ↦ e)

add_empt

theorem insSortCorrect : Sorted xs.insSort ∧ xs.Perm xs.insSort :=
  Empty.elim empt