-- 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.h₂.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 : Nat
ys : List Nat
u : Nat
us : List Nat
h₂ : insert x ys = u :: us
v : Nat
vs : List Nat
h₃ : insert z ys = v :: vs
⊢ evalList α ctx (z :: u :: us) = evalList α ctx (x :: v :: vs)

Tactic:
simp [evalList, ←h₂, ←h₃, evalList_insert ctx h]

Result:
case cons.h₂.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 : Nat
ys : List Nat
u : Nat
us : List Nat
h₂ : insert x ys = u :: us
v : Nat
vs : List Nat
h₃ : insert z ys = v :: vs
⊢ EvalInformation.evalOp ctx (EvalInformation.evalVar ctx z) (evalList α ctx (x :: ys)) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x) (evalList α ctx (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
⊢ ctx.op (EvalInformation.evalVar ctx z) (ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (head✝ :: tail✝))) =
    ctx.op (EvalInformation.evalVar ctx x) (ctx.op (EvalInformation.evalVar ctx z) (evalList α ctx (head✝ :: tail✝)))

Tactic:
rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]

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
⊢ insert x (insert z ys) ≠ []

Tactic:
simp [insert_nonEmpty]

Result:
no goals

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

Tactic:
cases ys

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

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

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

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, h.1, EvalInformation.evalOp]

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

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]

Result:
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
⊢ ctx.op (EvalInformation.evalVar ctx z) (ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (head✝ :: tail✝))) =
    ctx.op (EvalInformation.evalVar ctx x) (ctx.op (EvalInformation.evalVar ctx z) (evalList α ctx (head✝ :: tail✝)))

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 = []
⊢ evalList α ctx (z :: u :: us) = evalList α ctx [x]

Tactic:
apply absurd h₃

Result:
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 = []

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 = []
⊢ ¬insert x ys = []

Tactic:
simp [insert_nonEmpty]

Result:
no goals