-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.evalList_insert
  (ctx : Context α)
  (h : Commutative ctx.op)
  (x : Nat)
  (xs : List Nat)
  : evalList α ctx (insert x xs) = evalList α ctx (x::xs)

Proof state:
case single.isFalse
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x a✝ : Nat
h✝ : ¬x < a✝
⊢ evalList α ctx [a✝, x] = evalList α ctx [x, a✝]

Tactic:
simp [evalList, h.1, EvalInformation.evalOp]

Result:
no goals

Proof state:
case single.isFalse
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x a✝ : Nat
h✝ : ¬x < a✝
⊢ evalList α ctx [a✝, x] = evalList α ctx [x, a✝]

Tactic:
. simp [evalList, h.1, EvalInformation.evalOp]

Result:
no goals

Proof state:
case single.isTrue
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x a✝ : Nat
h✝ : x < a✝
⊢ evalList α ctx [x, a✝] = evalList α ctx [x, a✝]

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝ : x < y
⊢ evalList α ctx (x :: y :: z :: zs) = evalList α ctx (x :: y :: z :: zs)

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (z :: insert x zs) = ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (z :: zs))
h✝¹ : y ≤ x
h✝ : z ≤ x
⊢ ctx.op (EvalInformation.evalVar ctx y) (ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (z :: zs))) =
    ctx.op (EvalInformation.evalVar ctx x) (ctx.op (EvalInformation.evalVar ctx y) (evalList α ctx (z :: zs)))

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

Result:
no goals

Proof state:
case single
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x a✝ : Nat
⊢ evalList α ctx (if x < a✝ then [x, a✝] else [a✝, x]) = evalList α ctx [x, a✝]

Tactic:
split

Result:
case single.isTrue
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x a✝ : Nat
h✝ : x < a✝
⊢ evalList α ctx [x, a✝] = evalList α ctx [x, a✝]

case single.isFalse
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x a✝ : Nat
h✝ : ¬x < a✝
⊢ evalList α ctx [a✝, x] = evalList α ctx [x, a✝]

Proof state:
case single.isTrue
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x a✝ : Nat
h✝ : x < a✝
⊢ evalList α ctx [x, a✝] = evalList α ctx [x, a✝]

case single.isFalse
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x a✝ : Nat
h✝ : ¬x < a✝
⊢ evalList α ctx [a✝, x] = evalList α ctx [x, a✝]

Tactic:
. rfl

Result:
case single.isFalse
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x a✝ : Nat
h✝ : ¬x < a✝
⊢ evalList α ctx [a✝, x] = evalList α ctx [x, a✝]

Proof state:
case step
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
⊢ evalList α ctx (if x < y then x :: y :: z :: zs else y :: if x < z then x :: z :: zs else z :: insert x zs) =
    evalList α ctx (x :: y :: z :: zs)

Tactic:
split

Result:
case step.isTrue
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝ : x < y
⊢ evalList α ctx (x :: y :: z :: zs) = evalList α ctx (x :: y :: z :: zs)

case step.isFalse
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝ : ¬x < y
⊢ evalList α ctx (y :: if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)

Proof state:
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝ : ¬x < y
⊢ evalList α ctx (y :: if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)

Tactic:
split

Result:
case isTrue
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : x < z
⊢ evalList α ctx (y :: x :: z :: zs) = evalList α ctx (x :: y :: z :: zs)

case isFalse
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : ¬x < z
⊢ evalList α ctx (y :: z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)

Proof state:
case single
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x a✝ : Nat
⊢ evalList α ctx (insert x [a✝]) = evalList α ctx [x, a✝]

Tactic:
simp [insert]

Result:
case single
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x a✝ : Nat
⊢ evalList α ctx (if x < a✝ then [x, a✝] else [a✝, x]) = evalList α ctx [x, a✝]

Proof state:
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : x < z
⊢ evalList α ctx (y :: x :: z :: zs) = evalList α ctx (x :: y :: z :: zs)

Tactic:
simp [evalList, EvalInformation.evalOp]

Result:
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : x < z
⊢ ctx.op (EvalInformation.evalVar ctx y) (ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (z :: zs))) =
    ctx.op (EvalInformation.evalVar ctx x) (ctx.op (EvalInformation.evalVar ctx y) (evalList α ctx (z :: zs)))

Proof state:
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
h✝¹ : ¬x < y
h✝ : ¬x < z
⊢ evalList α ctx (y :: z :: insert x zs) = evalList α ctx (x :: y :: z :: zs)

Tactic:
simp_all [evalList, EvalInformation.evalOp]

Result:
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (z :: insert x zs) = ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (z :: zs))
h✝¹ : y ≤ x
h✝ : z ≤ x
⊢ ctx.op (EvalInformation.evalVar ctx y) (ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (z :: zs))) =
    ctx.op (EvalInformation.evalVar ctx x) (ctx.op (EvalInformation.evalVar ctx y) (evalList α ctx (z :: zs)))

Proof state:
case empty
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x : Nat
⊢ evalList α ctx (insert x []) = evalList α ctx [x]

Tactic:
rfl

Result:
no goals

Proof state:
case step
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (insert x (z :: zs)) = evalList α ctx (x :: z :: zs)
⊢ evalList α ctx (insert x (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

Tactic:
simp [insert] at *

Result:
case step
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (if x < z then x :: z :: zs else z :: insert x zs) = evalList α ctx (x :: z :: zs)
⊢ evalList α ctx (if x < y then x :: y :: z :: zs else y :: if x < z then x :: z :: zs else z :: insert x zs) =
    evalList α ctx (x :: y :: z :: zs)