-- 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.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]

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

Result:
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:
case single
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
a✝ : Nat
⊢ evalList α ctx (mergeIdem [a✝]) = evalList α ctx [a✝]

Tactic:
rfl

Result:
no goals

Proof state:
case step.cons
α : 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)
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

Tactic:
by_cases h₂ : x = y

Result:
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
⊢ evalList α ctx (mergeIdem (x :: 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
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

Proof state:
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
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

Tactic:
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 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
⊢ evalList α ctx (mergeIdem (x :: 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
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

Tactic:
case pos =>
  rw [h₂, mergeIdem_head, ih]
  simp [evalList, ←ctx.assoc.1, h.1, EvalInformation.evalOp]

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
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

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 (mergeIdem [x, y]) = evalList α ctx [x, y]

Tactic:
simp [mergeIdem, mergeIdem.loop]

Result:
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]

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

Tactic:
rw [ih]

Result:
no goals

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 (y :: z :: zs) = evalList α ctx (y :: y :: z :: zs)

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

Result:
no goals

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

Tactic:
exact val.down

Result:
no goals

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 (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:
by_cases h₃ : y = z

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

Proof state:
case empty
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IdempotentOp ctx.op
⊢ evalList α ctx (mergeIdem []) = evalList α ctx []

Tactic:
rfl

Result:
no goals

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
h₃ : y = z
⊢ evalList α ctx (x :: mergeIdem (z :: zs)) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x)
      (EvalInformation.evalOp ctx (EvalInformation.evalVar ctx z) (evalList α ctx (z :: zs)))

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

Result:
no goals