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

Proof state:
case step.nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
⊢ evalList α ctx (if x = y then [x] else [x, y]) = evalList α ctx [x, y]

Tactic:
split

Result:
case step.nil.isTrue
α : Sort u_1
ctx : Context α
h✝¹ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
h✝ : x = y
⊢ evalList α ctx [x] = evalList α ctx [x, y]

case step.nil.isFalse
α : Sort u_1
ctx : Context α
h✝¹ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
h✝ : ¬x = y
⊢ evalList α ctx [x, y] = evalList α ctx [x, y]

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

Tactic:
simp [h₂] at h

Result:
no goals

Proof state:
case step.nil.isFalse
α : Sort u_1
ctx : Context α
h✝¹ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
h✝ : ¬x = y
⊢ evalList α ctx [x, y] = evalList α ctx [x, y]

Tactic:
next => rfl

Result:
no goals

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

Tactic:
have h : IdempotentOp ctx.op := by
  simp [ContextInformation.isIdem, Option.isSome] at h;
  match h₂ : ctx.idem with
  | none =>
    simp [h₂] at h
  | some val =>
    simp [h₂] at h
    exact val.down

Result:
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
e : List Nat
h : IdempotentOp ctx.op
⊢ evalList α ctx (mergeIdem e) = evalList α ctx e

Proof state:
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : x = y
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

Tactic:
rw [h₂, mergeIdem_head, ih]

Result:
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : x = y
⊢ evalList α ctx (y :: z :: zs) = evalList α ctx (y :: y :: z :: zs)

Proof state:
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ x ≠ y

Tactic:
assumption

Result:
no goals

Proof state:
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
h₂ : x = y
⊢ evalList α ctx [x] = evalList α ctx [x, y]

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

Result:
no goals

Proof state:
case pos
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

case neg
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : ¬y = z
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ x ≠ y

Tactic:
case pos =>
  simp [mergeIdem_head, h₃, evalList]
  cases h₄ : mergeIdem (z :: zs) with
  | nil => apply absurd h₄; apply mergeIdem_nonEmpty; simp
  | cons u us => simp_all [mergeIdem, mergeIdem.loop, evalList]

Result:
case neg
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : ¬y = z
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ x ≠ y

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

Tactic:
cases ys with
| nil =>
  simp [mergeIdem, mergeIdem.loop]
  split
  next h₂ => simp [evalList, h₂, h.1, EvalInformation.evalOp]
  next => rfl
| cons z zs =>
  by_cases h₂ : x = y
  case pos =>
    rw [h₂, mergeIdem_head, ih]
    simp [evalList, ←ctx.assoc.1, h.1, EvalInformation.evalOp]
  case neg =>
    rw [mergeIdem_head2]
    by_cases h₃ : y = z
    case pos =>
      simp [mergeIdem_head, h₃, evalList]
      cases h₄ : mergeIdem (z :: zs) with
      | nil => apply absurd h₄; apply mergeIdem_nonEmpty; simp
      | cons u us => simp_all [mergeIdem, mergeIdem.loop, evalList]
    case neg =>
      simp [mergeIdem_head2, h₃, evalList] at *
      rw [ih]
    assumption

Result:
no goals

Proof state:
case nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
h₄ : mergeIdem (z :: zs) = []
⊢ ¬mergeIdem (z :: zs) = []

Tactic:
apply mergeIdem_nonEmpty

Result:
case nil.h
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
h₄ : mergeIdem (z :: zs) = []
⊢ z :: zs ≠ []

Proof state:
case nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
h₄ : mergeIdem (z :: zs) = []
⊢ evalList α ctx [x] =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x)
      (EvalInformation.evalOp ctx (EvalInformation.evalVar ctx z) (evalList α ctx (z :: zs)))

Tactic:
apply absurd h₄

Result:
case nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
h₄ : mergeIdem (z :: zs) = []
⊢ ¬mergeIdem (z :: zs) = []