-- 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:
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))

Tactic:
simp [sort.loop, ←ih]

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 (sort.loop (insert x (insert z ys)) zs)

Proof state:
case cons.h₂.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
h₂ : insert x ys = []
⊢ evalList α ctx [z] = evalList α ctx (x :: insert z ys)

Tactic:
apply absurd h₂

Result:
case cons.h₂.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
h₂ : insert x ys = []
⊢ ¬insert x ys = []

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 (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:
cases h₂ : insert x ys with
| nil => apply absurd h₂; simp [insert_nonEmpty]
| cons u us =>
  cases h₃ : insert z ys with
  | nil => apply absurd h₃; simp [insert_nonEmpty]
  | cons v vs =>
    simp [evalList, ←h₂, ←h₃, evalList_insert ctx h]
    cases ys
    . simp [evalList, h.1, EvalInformation.evalOp]
    . simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]

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
⊢ 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:
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x : Nat
xs ys : List Nat
⊢ evalList α ctx (sort.loop (insert x ys) xs) = evalList α ctx (x :: sort.loop ys xs)

Tactic:
induction xs generalizing x ys with
| nil => simp [sort.loop, evalList_insert ctx h]
| cons z zs ih =>
  rw [evalList_sort_loop_swap ctx h]; simp [sort.loop, ←ih]; apply evalList_sort_congr ctx h; rw [evalList_insert ctx h]
  cases h₂ : insert x ys with
  | nil => apply absurd h₂; simp [insert_nonEmpty]
  | cons u us =>
    cases h₃ : insert z ys with
    | nil => apply absurd h₃; simp [insert_nonEmpty]
    | cons v vs =>
      simp [evalList, ←h₂, ←h₃, evalList_insert ctx h]
      cases ys
      . simp [evalList, h.1, EvalInformation.evalOp]
      . simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
  all_goals 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
⊢ 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:
all_goals simp [insert_nonEmpty]

Result:
no goals

Proof state:
case cons.h₂.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
u : Nat
us : List Nat
h₂ : insert x ys = u :: us
⊢ evalList α ctx (z :: u :: us) = evalList α ctx (x :: insert z ys)

Tactic:
cases h₃ : insert z ys with
| nil => apply absurd h₃; simp [insert_nonEmpty]
| cons v vs =>
  simp [evalList, ←h₂, ←h₃, evalList_insert ctx h]
  cases ys
  . simp [evalList, h.1, EvalInformation.evalOp]
  . simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]

Result:
no goals

Proof state:
case nil
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x : Nat
ys : List Nat
⊢ evalList α ctx (sort.loop (insert x ys) []) = evalList α ctx (x :: sort.loop ys [])

Tactic:
simp [sort.loop, evalList_insert ctx h]

Result:
no goals

Proof state:
α : 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)

Tactic:
generalize [] = ys

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

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 (z :: insert x ys) zs) = evalList α ctx (sort.loop (insert x (insert z ys)) zs)

Tactic:
apply evalList_sort_congr 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 (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) ≠ []