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

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

Result:
no goals

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

Tactic:
induction ys generalizing y xs with
| nil => simp [sort.loop, evalList_insert ctx h]
| cons z zs _  =>
  simp [sort.loop]; apply evalList_sort_congr ctx h
  simp [evalList_insert ctx h]
  cases h₂ : insert y xs
  . apply absurd h₂; simp [insert_nonEmpty]
  . simp [evalList, ←h₂, evalList_insert ctx h]
  all_goals simp [insert_nonEmpty]

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 = []
⊢ ¬insert y xs = []

Tactic:
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
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:
. simp [evalList, ←h₂, evalList_insert 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
⊢ 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
α : 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 xs (y :: z :: zs)) = evalList α ctx (sort.loop (y :: xs) (z :: zs))

Tactic:
simp [sort.loop]

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

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 (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) ≠ []

Tactic:
simp [evalList_insert 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 (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) ≠ []

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)

Tactic:
apply absurd h₂

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 = []
⊢ ¬insert 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
⊢ insert z (y :: xs) ≠ []

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
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:
all_goals simp [insert_nonEmpty]

Result:
no goals