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

Tactic:
next => rfl

Result:
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 : Nat
xs : List Nat
⊢ evalList α ctx (insert x xs) = evalList α ctx (x :: xs)

Tactic:
induction xs using List.two_step_induction with
| empty => rfl
| single =>
  simp [insert]
  split
  . rfl
  . simp [evalList, h.1, EvalInformation.evalOp]
| step y z zs ih =>
  simp [insert] at *; split
  next => rfl
  next =>
    split
    next => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
    next => simp_all [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]

Result:
no goals

Proof state:
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)

Tactic:
next =>
  split
  next => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
  next => simp_all [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]

Result:
no goals

Proof state:
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)

Tactic:
next => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]

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

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

Result:
no goals

Proof state:
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)

Tactic:
next => simp_all [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]

Result:
no goals