-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.evalList_sort_congr
  (ctx : Context α)
  (h : Commutative ctx.op)
  (h₂ : evalList α ctx a = evalList α ctx b)
  (h₃ : a ≠ [])
  (h₄ : b ≠ [])
  : evalList α ctx (sort.loop a c) = evalList α ctx (sort.loop b c)

Proof state:
case cons.h₂
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (insert c a) = evalList α ctx (insert c b)

case cons.h₃
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c a ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c b ≠ []

Tactic:
simp [evalList_insert ctx h, evalList]

Result:
case cons.h₂
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (c :: a) = evalList α ctx (c :: b)

case cons.h₃
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c a ≠ []

case cons.h₄
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ insert c b ≠ []

Proof state:
case cons.h₂.cons.cons
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a : Nat
as : List Nat
h₃ : a :: as ≠ []
b : Nat
bs : List Nat
h₄ : b :: bs ≠ []
h₂ : evalList α ctx (a :: as) = evalList α ctx (b :: bs)
⊢ evalList α ctx (c :: a :: as) = evalList α ctx (c :: b :: bs)

Tactic:
simp [evalList, h₂]

Result:
no goals

Proof state:
case cons.h₂.cons.nil
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a : Nat
as : List Nat
h₃ : a :: as ≠ []
h₄ : [] ≠ []
h₂ : evalList α ctx (a :: as) = evalList α ctx []
⊢ ¬[] ≠ []

Tactic:
simp

Result:
no goals

Proof state:
case cons.h₂.cons
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
b : List Nat
h₄ : b ≠ []
a : Nat
as : List Nat
h₂ : evalList α ctx (a :: as) = evalList α ctx b
h₃ : a :: as ≠ []
⊢ evalList α ctx (c :: a :: as) = evalList α ctx (c :: b)

Tactic:
cases b with
| nil => apply absurd h₄; simp
| cons b bs => simp [evalList, h₂]

Result:
no goals

Proof state:
case cons.h₂.nil
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
b : List Nat
h₄ : b ≠ []
h₂ : evalList α ctx [] = evalList α ctx b
h₃ : [] ≠ []
⊢ evalList α ctx [c] = evalList α ctx (c :: b)

Tactic:
apply absurd h₃

Result:
case cons.h₂.nil
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
b : List Nat
h₄ : b ≠ []
h₂ : evalList α ctx [] = evalList α ctx b
h₃ : [] ≠ []
⊢ ¬[] ≠ []

Proof state:
case nil
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
a b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (sort.loop a []) = evalList α ctx (sort.loop b [])

Tactic:
simp [sort.loop, h₂]

Result:
no goals

Proof state:
case cons.h₂.cons.nil
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a : Nat
as : List Nat
h₃ : a :: as ≠ []
h₄ : [] ≠ []
h₂ : evalList α ctx (a :: as) = evalList α ctx []
⊢ evalList α ctx (c :: a :: as) = evalList α ctx [c]

Tactic:
apply absurd h₄

Result:
case cons.h₂.cons.nil
α : Sort u_1
ctx : Context α
h : Commutative ctx.op
c : Nat
tail✝ : List Nat
ih :
  ∀ {a b : List Nat},
    evalList α ctx a = evalList α ctx b →
      a ≠ [] → b ≠ [] → evalList α ctx (sort.loop a tail✝) = evalList α ctx (sort.loop b tail✝)
a : Nat
as : List Nat
h₃ : a :: as ≠ []
h₄ : [] ≠ []
h₂ : evalList α ctx (a :: as) = evalList α ctx []
⊢ ¬[] ≠ []