-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.evalList_sort (ctx : Context α) (h : ContextInformation.isComm ctx) (e : List Nat) : evalList α ctx (sort e) = evalList α ctx e

Proof state:
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
e : List Nat
h : Commutative ctx.op
⊢ evalList α ctx (sort e) = evalList α ctx e

Tactic:
induction e using List.two_step_induction with
| empty => rfl
| single => rfl
| step x y ys ih =>
  simp [evalList_sort_cons ctx h]
  cases h₂ : sort (y :: ys) with
  | nil => simp [sort, sort.loop] at *; apply absurd h₂; apply sort_loop_nonEmpty; apply insert_nonEmpty
  | cons z zs => simp [evalList, ←h₂, ih]

Result:
no goals

Proof state:
α : Sort u_1
ctx : Context α
h : ContextInformation.isComm ctx = true
e : List Nat
⊢ Commutative ctx.op

Tactic:
simp [ContextInformation.isComm, Option.isSome] at h

Result:
α : Sort u_1
ctx : Context α
h :
  (match ctx.comm with
    | some val => true
    | none => false) =
    true
e : List Nat
⊢ Commutative ctx.op

Proof state:
case step.cons
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
x y : Nat
ys : List Nat
ih : evalList α ctx (sort (y :: ys)) = evalList α ctx (y :: ys)
z : Nat
zs : List Nat
h₂ : sort (y :: ys) = z :: zs
⊢ evalList α ctx (x :: z :: zs) = evalList α ctx (x :: y :: ys)

Tactic:
simp [evalList, ←h₂, ih]

Result:
no goals

Proof state:
case step.nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
x y : Nat
ys : List Nat
ih : evalList α ctx (sort (y :: ys)) = evalList α ctx (y :: ys)
h₂ : sort (y :: ys) = []
⊢ evalList α ctx [x] = evalList α ctx (x :: y :: ys)

Tactic:
simp [sort, sort.loop] at *

Result:
case step.nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
x y : Nat
ys : List Nat
ih : evalList α ctx (sort.loop (insert y []) ys) = evalList α ctx (y :: ys)
h₂ : sort.loop (insert y []) ys = []
⊢ evalList α ctx [x] = evalList α ctx (x :: y :: ys)

Proof state:
α : Sort u_1
ctx : Context α
h :
  (match ctx.comm with
    | some val => true
    | none => false) =
    true
e : List Nat
val : PLift (Commutative ctx.op)
h₂ : ctx.comm = some val
⊢ Commutative ctx.op

Tactic:
simp [h₂] at h

Result:
α : Sort u_1
ctx : Context α
e : List Nat
val : PLift (Commutative ctx.op)
h₂ : ctx.comm = some val
h : True
⊢ Commutative ctx.op

Proof state:
α : Sort u_1
ctx : Context α
h :
  (match ctx.comm with
    | some val => true
    | none => false) =
    true
e : List Nat
h₂ : ctx.comm = none
⊢ Commutative ctx.op

Tactic:
simp [h₂] at h

Result:
no goals

Proof state:
case step
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
x y : Nat
ys : List Nat
ih : evalList α ctx (sort (y :: ys)) = evalList α ctx (y :: ys)
⊢ evalList α ctx (x :: sort (y :: ys)) = evalList α ctx (x :: y :: ys)

Tactic:
cases h₂ : sort (y :: ys) with
| nil => simp [sort, sort.loop] at *; apply absurd h₂; apply sort_loop_nonEmpty; apply insert_nonEmpty
| cons z zs => simp [evalList, ←h₂, ih]

Result:
no goals

Proof state:
case step.nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
x y : Nat
ys : List Nat
ih : evalList α ctx (sort.loop (insert y []) ys) = evalList α ctx (y :: ys)
h₂ : sort.loop (insert y []) ys = []
⊢ evalList α ctx [x] = evalList α ctx (x :: y :: ys)

Tactic:
apply absurd h₂

Result:
case step.nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
x y : Nat
ys : List Nat
ih : evalList α ctx (sort.loop (insert y []) ys) = evalList α ctx (y :: ys)
h₂ : sort.loop (insert y []) ys = []
⊢ ¬sort.loop (insert y []) ys = []

Proof state:
α : Sort u_1
ctx : Context α
h :
  (match ctx.comm with
    | some val => true
    | none => false) =
    true
e : List Nat
⊢ Commutative ctx.op

Tactic:
match h₂ : ctx.comm with
| none =>
  simp [h₂] at h
| some val =>
  simp [h₂] at h
  exact val.down

Result:
no goals

Proof state:
case step
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
x y : Nat
ys : List Nat
ih : evalList α ctx (sort (y :: ys)) = evalList α ctx (y :: ys)
⊢ evalList α ctx (sort (x :: y :: ys)) = evalList α ctx (x :: y :: ys)

Tactic:
simp [evalList_sort_cons ctx h]

Result:
case step
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
x y : Nat
ys : List Nat
ih : evalList α ctx (sort (y :: ys)) = evalList α ctx (y :: ys)
⊢ evalList α ctx (x :: sort (y :: ys)) = evalList α ctx (x :: y :: ys)

Proof state:
case step.nil.h
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
x y : Nat
ys : List Nat
ih : evalList α ctx (sort.loop (insert y []) ys) = evalList α ctx (y :: ys)
h₂ : sort.loop (insert y []) ys = []
⊢ insert y [] ≠ []

Tactic:
apply insert_nonEmpty

Result:
no goals

Proof state:
α : Sort u_1
ctx : Context α
h : ContextInformation.isComm ctx = true
e : List Nat
⊢ evalList α ctx (sort e) = evalList α ctx e

Tactic:
have h : Commutative ctx.op := by
  simp [ContextInformation.isComm, Option.isSome] at h
  match h₂ : ctx.comm with
  | none =>
    simp [h₂] at h
  | some val =>
    simp [h₂] at h
    exact val.down

Result:
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
e : List Nat
h : Commutative ctx.op
⊢ evalList α ctx (sort e) = evalList α ctx e

Proof state:
case single
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
a✝ : Nat
⊢ evalList α ctx (sort [a✝]) = evalList α ctx [a✝]

Tactic:
rfl

Result:
no goals

Proof state:
case empty
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
⊢ evalList α ctx (sort []) = evalList α ctx []

Tactic:
rfl

Result:
no goals

Proof state:
case step.nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
x y : Nat
ys : List Nat
ih : evalList α ctx (sort.loop (insert y []) ys) = evalList α ctx (y :: ys)
h₂ : sort.loop (insert y []) ys = []
⊢ ¬sort.loop (insert y []) ys = []

Tactic:
apply sort_loop_nonEmpty

Result:
case step.nil.h
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isComm ctx = true
h : Commutative ctx.op
x y : Nat
ys : List Nat
ih : evalList α ctx (sort.loop (insert y []) ys) = evalList α ctx (y :: ys)
h₂ : sort.loop (insert y []) ys = []
⊢ insert y [] ≠ []

Proof state:
α : Sort u_1
ctx : Context α
e : List Nat
val : PLift (Commutative ctx.op)
h₂ : ctx.comm = some val
h : True
⊢ Commutative ctx.op

Tactic:
exact val.down

Result:
no goals