-- 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:
α : Sort u_1
a b c : List Nat
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)

Tactic:
induction c generalizing a b with
| nil => simp [sort.loop, h₂]
| cons c _  ih =>
  simp [sort.loop]; apply ih; simp [evalList_insert ctx h, evalList]
  cases a with
  | nil => apply absurd h₃; simp
  | cons a as =>
    cases b with
    | nil => apply absurd h₄; simp
    | cons b bs => simp [evalList, h₂]
  all_goals apply insert_nonEmpty

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₃ : [] ≠ []
⊢ ¬[] ≠ []

Tactic:
simp

Result:
no goals

Proof state:
case 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 b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (sort.loop a (c :: tail✝)) = evalList α ctx (sort.loop b (c :: tail✝))

Tactic:
simp [sort.loop]

Result:
case 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 b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (sort.loop (insert c a) tail✝) = evalList α ctx (sort.loop (insert c b) tail✝)

Proof state:
case 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 b : List Nat
h₂ : evalList α ctx a = evalList α ctx b
h₃ : a ≠ []
h₄ : b ≠ []
⊢ evalList α ctx (sort.loop (insert c a) tail✝) = evalList α ctx (sort.loop (insert c b) tail✝)

Tactic:
apply ih

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 (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 ≠ []

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 (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 ≠ []

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

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 ≠ []
⊢ 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₃
α : 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:
all_goals apply insert_nonEmpty

Result:
no goals

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 ≠ []
⊢ insert c b ≠ []

Tactic:
apply insert_nonEmpty

Result:
no goals