-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.evalList_sort_cons
  (ctx : Context α)
  (h : Commutative ctx.op)
  (x : Nat)
  (xs : List Nat)
  : evalList α ctx (sort (x :: xs)) = evalList α ctx (x :: sort xs)

Proof state:
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x : Nat
xs : List Nat
⊢ evalList α ctx (sort (x :: xs)) = evalList α ctx (x :: sort xs)

Tactic:
simp [sort, sort.loop]

Result:
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x : Nat
xs : List Nat
⊢ evalList α ctx (sort.loop (insert x []) xs) = evalList α ctx (x :: sort.loop [] xs)

Proof state:
case cons.h₂.cons.nil
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
ih : ∀ (x : Nat) (ys : List Nat), evalList α ctx (sort.loop (insert x ys) zs) = evalList α ctx (x :: sort.loop ys zs)
x : Nat
ys : List Nat
u : Nat
us : List Nat
h₂ : insert x ys = u :: us
h₃ : insert z ys = []
⊢ ¬insert z ys = []

Tactic:
simp [insert_nonEmpty]

Result:
no goals

Proof state:
case cons.h₂
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
ih : ∀ (x : Nat) (ys : List Nat), evalList α ctx (sort.loop (insert x ys) zs) = evalList α ctx (x :: sort.loop ys zs)
x : Nat
ys : List Nat
⊢ evalList α ctx (z :: insert x ys) = evalList α ctx (insert x (insert z ys))

case cons.h₃
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
ih : ∀ (x : Nat) (ys : List Nat), evalList α ctx (sort.loop (insert x ys) zs) = evalList α ctx (x :: sort.loop ys zs)
x : Nat
ys : List Nat
⊢ z :: insert x ys ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
ih : ∀ (x : Nat) (ys : List Nat), evalList α ctx (sort.loop (insert x ys) zs) = evalList α ctx (x :: sort.loop ys zs)
x : Nat
ys : List Nat
⊢ insert x (insert z ys) ≠ []

Tactic:
rw [evalList_insert ctx h]

Result:
case cons.h₂
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
ih : ∀ (x : Nat) (ys : List Nat), evalList α ctx (sort.loop (insert x ys) zs) = evalList α ctx (x :: sort.loop ys zs)
x : Nat
ys : List Nat
⊢ evalList α ctx (z :: insert x ys) = evalList α ctx (x :: insert z ys)

case cons.h₃
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
ih : ∀ (x : Nat) (ys : List Nat), evalList α ctx (sort.loop (insert x ys) zs) = evalList α ctx (x :: sort.loop ys zs)
x : Nat
ys : List Nat
⊢ z :: insert x ys ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
ih : ∀ (x : Nat) (ys : List Nat), evalList α ctx (sort.loop (insert x ys) zs) = evalList α ctx (x :: sort.loop ys zs)
x : Nat
ys : List Nat
⊢ insert x (insert z ys) ≠ []

Proof state:
case cons.h₂.cons.cons.cons
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
ih : ∀ (x : Nat) (ys : List Nat), evalList α ctx (sort.loop (insert x ys) zs) = evalList α ctx (x :: sort.loop ys zs)
x u : Nat
us : List Nat
v : Nat
vs : List Nat
head✝ : Nat
tail✝ : List Nat
h₂ : insert x (head✝ :: tail✝) = u :: us
h₃ : insert z (head✝ :: tail✝) = v :: vs
⊢ EvalInformation.evalOp ctx (EvalInformation.evalVar ctx z) (evalList α ctx (x :: head✝ :: tail✝)) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x) (evalList α ctx (z :: head✝ :: tail✝))

Tactic:
. simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]

Result:
no goals

Proof state:
case cons.h₂.cons.cons.nil
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
ih : ∀ (x : Nat) (ys : List Nat), evalList α ctx (sort.loop (insert x ys) zs) = evalList α ctx (x :: sort.loop ys zs)
x u : Nat
us : List Nat
v : Nat
vs : List Nat
h₂ : insert x [] = u :: us
h₃ : insert z [] = v :: vs
⊢ EvalInformation.evalOp ctx (EvalInformation.evalVar ctx z) (evalList α ctx [x]) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x) (evalList α ctx [z])

Tactic:
simp [evalList, h.1, EvalInformation.evalOp]

Result:
no goals

Proof state:
case cons
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
ih : ∀ (x : Nat) (ys : List Nat), evalList α ctx (sort.loop (insert x ys) zs) = evalList α ctx (x :: sort.loop ys zs)
x : Nat
ys : List Nat
⊢ evalList α ctx (sort.loop (insert x ys) (z :: zs)) = evalList α ctx (x :: sort.loop ys (z :: zs))

Tactic:
rw [evalList_sort_loop_swap ctx h]

Result:
case cons
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
ih : ∀ (x : Nat) (ys : List Nat), evalList α ctx (sort.loop (insert x ys) zs) = evalList α ctx (x :: sort.loop ys zs)
x : Nat
ys : List Nat
⊢ evalList α ctx (sort.loop (z :: insert x ys) zs) = evalList α ctx (x :: sort.loop ys (z :: zs))