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

Tactic:
simp [mergeIdem_head, h₃, evalList]

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

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

Tactic:
match h₂ : ctx.idem with
| none =>
  simp [h₂] at h
| some val =>
  simp [h₂] at h
  exact val.down

Result:
no goals

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

Tactic:
induction e using List.two_step_induction with
| empty => rfl
| single => rfl
| step x y ys ih =>
  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:
α : Sort u_1
ctx : Context α
h :
  (match ctx.idem with
    | some val => true
    | none => false) =
    true
e : List Nat
val : PLift (IdempotentOp ctx.op)
h₂ : ctx.idem = some val
⊢ IdempotentOp ctx.op

Tactic:
simp [h₂] at h

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

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

Tactic:
simp [mergeIdem_head2, h₃, evalList] at *

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

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 [mergeIdem_head2]

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 (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 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 neg =>
  simp [mergeIdem_head2, h₃, evalList] at *
  rw [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
⊢ x ≠ y

Proof state:
α : Sort u_1
ctx : Context α
h : ContextInformation.isIdem ctx = true
e : List Nat
⊢ IdempotentOp ctx.op

Tactic:
simp [ContextInformation.isIdem, Option.isSome] at h

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

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

Tactic:
rfl

Result:
no goals

Proof state:
case 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)
h₂ : ¬x = y
h₃ : y = z
u : Nat
us : List Nat
h₄ : mergeIdem (z :: zs) = u :: us
⊢ evalList α ctx (x :: u :: us) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x)
      (EvalInformation.evalOp ctx (EvalInformation.evalVar ctx z) (evalList α ctx (z :: zs)))

Tactic:
simp_all [mergeIdem, mergeIdem.loop, evalList]

Result:
no goals

Proof state:
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 ≠ []

Tactic:
simp

Result:
no goals