-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.evalList_append
  (ctx : Context α)
  (l r : List Nat)
  (h₁ : l ≠ [])
  (h₂ : r ≠ [])
  : evalList α ctx (l.append r) = ctx.op (evalList α ctx l) (evalList α ctx r)

Proof state:
case single.cons
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
head✝ : Nat
tail✝ : List Nat
h₂ : head✝ :: tail✝ ≠ []
⊢ evalList α ctx ([x].append (head✝ :: tail✝)) = ctx.op (evalList α ctx [x]) (evalList α ctx (head✝ :: tail✝))

Tactic:
. simp [List.append, evalList, EvalInformation.evalOp]

Result:
no goals

Proof state:
case step
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : r ≠ []
x y : Nat
ys : List Nat
ih : y :: ys ≠ [] → evalList α ctx ((y :: ys).append r) = ctx.op (evalList α ctx (y :: ys)) (evalList α ctx r)
h₁ : x :: y :: ys ≠ []
⊢ evalList α ctx ((x :: y :: ys).append r) = ctx.op (evalList α ctx (x :: y :: ys)) (evalList α ctx r)

Tactic:
simp [List.append, evalList, EvalInformation.evalOp] at *

Result:
case step
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : ¬r = []
x y : Nat
ys : List Nat
ih : evalList α ctx (y :: (ys ++ r)) = ctx.op (evalList α ctx (y :: ys)) (evalList α ctx r)
h₁ : True
⊢ ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (y :: (ys ++ r))) =
    ctx.op (ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (y :: ys))) (evalList α ctx r)

Proof state:
case single.nil
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
h₂ : [] ≠ []
⊢ evalList α ctx ([x].append []) = ctx.op (evalList α ctx [x]) (evalList α ctx [])

case single.cons
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
head✝ : Nat
tail✝ : List Nat
h₂ : head✝ :: tail✝ ≠ []
⊢ evalList α ctx ([x].append (head✝ :: tail✝)) = ctx.op (evalList α ctx [x]) (evalList α ctx (head✝ :: tail✝))

Tactic:
. simp at h₂

Result:
case single.cons
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
head✝ : Nat
tail✝ : List Nat
h₂ : head✝ :: tail✝ ≠ []
⊢ evalList α ctx ([x].append (head✝ :: tail✝)) = ctx.op (evalList α ctx [x]) (evalList α ctx (head✝ :: tail✝))

Proof state:
case single.cons
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
head✝ : Nat
tail✝ : List Nat
h₂ : head✝ :: tail✝ ≠ []
⊢ evalList α ctx ([x].append (head✝ :: tail✝)) = ctx.op (evalList α ctx [x]) (evalList α ctx (head✝ :: tail✝))

Tactic:
simp [List.append, evalList, EvalInformation.evalOp]

Result:
no goals

Proof state:
case step
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : ¬r = []
x y : Nat
ys : List Nat
ih : evalList α ctx (y :: (ys ++ r)) = ctx.op (evalList α ctx (y :: ys)) (evalList α ctx r)
h₁ : True
⊢ ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (y :: (ys ++ r))) =
    ctx.op (ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (y :: ys))) (evalList α ctx r)

Tactic:
rw [ih]

Result:
case step
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : ¬r = []
x y : Nat
ys : List Nat
ih : evalList α ctx (y :: (ys ++ r)) = ctx.op (evalList α ctx (y :: ys)) (evalList α ctx r)
h₁ : True
⊢ ctx.op (EvalInformation.evalVar ctx x) (ctx.op (evalList α ctx (y :: ys)) (evalList α ctx r)) =
    ctx.op (ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (y :: ys))) (evalList α ctx r)

Proof state:
case step
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : ¬r = []
x y : Nat
ys : List Nat
ih : evalList α ctx (y :: (ys ++ r)) = ctx.op (evalList α ctx (y :: ys)) (evalList α ctx r)
h₁ : True
⊢ ctx.op (EvalInformation.evalVar ctx x) (ctx.op (evalList α ctx (y :: ys)) (evalList α ctx r)) =
    ctx.op (ctx.op (EvalInformation.evalVar ctx x) (evalList α ctx (y :: ys))) (evalList α ctx r)

Tactic:
simp [ctx.assoc.1]

Result:
no goals

Proof state:
case empty
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : r ≠ []
h₁ : [] ≠ []
⊢ evalList α ctx ([].append r) = ctx.op (evalList α ctx []) (evalList α ctx r)

Tactic:
simp_all

Result:
no goals

Proof state:
case single.nil
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
h₂ : [] ≠ []
⊢ evalList α ctx ([x].append []) = ctx.op (evalList α ctx [x]) (evalList α ctx [])

Tactic:
simp at h₂

Result:
no goals

Proof state:
α : Sort u_1
ctx : Context α
l r : List Nat
h₁ : l ≠ []
h₂ : r ≠ []
⊢ evalList α ctx (l.append r) = ctx.op (evalList α ctx l) (evalList α ctx r)

Tactic:
induction l using List.two_step_induction with
| empty => simp_all
| single x =>
  cases r
  . simp at h₂
  . simp [List.append, evalList, EvalInformation.evalOp]
| step x y ys ih => simp [List.append, evalList, EvalInformation.evalOp] at *; rw [ih]; simp [ctx.assoc.1]

Result:
no goals

Proof state:
case single
α : Sort u_1
ctx : Context α
r : List Nat
h₂ : r ≠ []
x : Nat
h₁ : [x] ≠ []
⊢ evalList α ctx ([x].append r) = ctx.op (evalList α ctx [x]) (evalList α ctx r)

Tactic:
cases r

Result:
case single.nil
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
h₂ : [] ≠ []
⊢ evalList α ctx ([x].append []) = ctx.op (evalList α ctx [x]) (evalList α ctx [])

case single.cons
α : Sort u_1
ctx : Context α
x : Nat
h₁ : [x] ≠ []
head✝ : Nat
tail✝ : List Nat
h₂ : head✝ :: tail✝ ≠ []
⊢ evalList α ctx ([x].append (head✝ :: tail✝)) = ctx.op (evalList α ctx [x]) (evalList α ctx (head✝ :: tail✝))