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

Proof state:
case cons
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ evalList α ctx (sort.loop (insert z (insert y xs)) zs) = evalList α ctx (sort.loop (insert z (y :: xs)) 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
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ evalList α ctx (insert z (insert y xs)) = evalList α ctx (insert z (y :: xs))

case cons.h₃
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []

Proof state:
case cons.h₂
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ evalList α ctx (z :: insert y xs) = evalList α ctx (z :: y :: xs)

case cons.h₃
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []

Tactic:
cases h₂ : insert y xs

Result:
case cons.h₂.nil
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
h₂ : insert y xs = []
⊢ evalList α ctx [z] = evalList α ctx (z :: y :: xs)

case cons.h₂.cons
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
head✝ : Nat
tail✝ : List Nat
h₂ : insert y xs = head✝ :: tail✝
⊢ evalList α ctx (z :: head✝ :: tail✝) = evalList α ctx (z :: y :: xs)

case cons.h₃
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []

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

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

Result:
no goals

Proof state:
case cons.h₂.nil
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
h₂ : insert y xs = []
⊢ evalList α ctx [z] = evalList α ctx (z :: y :: xs)

case cons.h₂.cons
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
head✝ : Nat
tail✝ : List Nat
h₂ : insert y xs = head✝ :: tail✝
⊢ evalList α ctx (z :: head✝ :: tail✝) = evalList α ctx (z :: y :: xs)

case cons.h₃
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []

Tactic:
. apply absurd h₂; simp [insert_nonEmpty]

Result:
case cons.h₂.cons
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
head✝ : Nat
tail✝ : List Nat
h₂ : insert y xs = head✝ :: tail✝
⊢ evalList α ctx (z :: head✝ :: tail✝) = evalList α ctx (z :: y :: xs)

case cons.h₃
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (insert y xs) ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
z : Nat
zs : List Nat
tail_ih✝ :
  ∀ {y : Nat} (xs : List Nat), evalList α ctx (sort.loop xs (y :: zs)) = evalList α ctx (sort.loop (y :: xs) zs)
y : Nat
xs : List Nat
⊢ insert z (y :: xs) ≠ []