Failure to generate unfold theorems

[hargoniX]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In the following rbtree formalisation the unfold del line towards the end fails to generate unfolding theorems:

/--
Colors of red black tree nodes.
-/
inductive Color where
  | black
  | red

/--
The basic red black tree data structure without any invariant etc. attached.
-/
inductive Raw (α : Type u) where
  /--
  The empty tree.
  -/
  | nil : Raw α
  /--
  A node with left and right successor, its color and a piece of data
  -/
  | node (left : Raw α) (data : α) (color : Color) (right : Raw α) : Raw α

namespace Raw

/--
Paint the color of the root of `t` to given color `c`.
-/
@[inline]
def paintColor (c : Color) (t : Raw α) : Raw α :=
  match t with
  | .nil => .nil
  | .node l d _ r => .node l d c r

-- Balanced insert into the left child, fixing red on red sequences on the way.
@[inline]
def baliL (d : α) : Raw α → Raw α → Raw α
  | .node (.node t₁ data₁ .red t₂) data₂ .red t₃, right
  | .node t₁ data₁ .red (.node t₂ data₂ .red t₃), right =>
      .node (.node t₁ data₁ .black t₂) data₂ .red (.node t₃ d .black right)
  | left, right => .node left d .black right

-- Balanced insert into the right child, fixing red on red sequences on the way.
@[inline]
def baliR (d : α) : Raw α → Raw α → Raw α
  | left, .node t₁ data₁ .red (.node t₂ data₂ .red t₃)
  | left, .node (.node t₁ data₁ .red t₂) data₂ .red t₃ =>
      .node (.node left d .black t₁) data₁ .red (.node t₂ data₂ .black t₃)
  | left, right => .node left d .black right

-- Balance a tree on the way up from deletion, prioritizing the left side.
def baldL (d : α) : Raw α → Raw α → Raw α
  | .node t₁ data .red t₂, right =>
      .node (.node t₁ data .black t₂) d .red right
  | left, .node t₁ data .black t₂ =>
      baliR d left (.node t₁ data .red t₂)
  | left, .node (.node t₁ data₁ .black t₂) data₂ .red t₃ =>
      .node (.node left d .black t₁) data₁ .red (baliR data₂ t₂ (paintColor .red t₃))
  | left, right => .node left d .red right

-- Balance a tree on the way up from deletion, prioritizing the right side.
def baldR (d : α) : Raw α → Raw α → Raw α
  | left, .node t₁ data .red t₂ =>
      .node left d .red (.node t₁ data .black t₂)
  | .node t₁ data .black t₂, right =>
      baliL d (.node t₁ data .red t₂) right
  | .node  t₁ data₁ .red (.node t₂ data₂ .black t₃), right =>
      .node (baliL data₁ (paintColor .red t₁) t₂) data₁ .red (.node t₃ data₂ .black right)
  | left, right => .node left d .red right

-- Appends one tree to another while painting the correct color
def appendTrees : Raw α → Raw α → Raw α
  | .nil, t => t
  | t, .nil => t
  | .node left₁ data₁ .red right₁, .node left₂ data₂ .red right₂ =>
    match appendTrees right₁ left₂ with
    | .node left₃ data₃ .red right₃ =>
        .node (.node left₁ data₁ .red left₃) data₃ .red (.node right₃ data₂ .red right₂)
    | t                   => .node left₁ data₁ .red (.node t data₂ .red right₂)
  | .node left₁ data₁ .black right₁, .node left₂ data₂ .black right₂ =>
    match appendTrees right₁ left₂ with
    | .node left₃ data₃ .red right₃ =>
        .node (node left₁ data₁ .black left₃) data₃ .red (node right₃ data₂ .black right₂)
    | t                   => baldL data₁ left₁ (node t data₂ .black right₂)
  | t, .node left data .red right => node (appendTrees t left) data .red right
  | .node left data .red right, t => .node left data .red (appendTrees right t)

def del [Ord α] (d : α) : Raw α → Raw α
  | .nil => .nil
  | .node left data _ right =>
    match compare d data with
    | .lt =>
      match left with
      | .node _ _ .black _ => baldL data (del d left) right
      | _ => .node (del d left) data .red right
    | .eq => appendTrees left right
    | .gt =>
      match right with
      | .node _ _ .black _ => baldR data left (del d right)
      | _ => .node left data .red (del d right)


example : del 1 .nil = .nil := by
  unfold del
end Raw

Expected behavior: unfold should just work

Actual behavior: [Clear and concise description of what actually happens]

Versions

Lean 4.16.0-nightly-2025-01-09
Target: x86_64-unknown-linux-gnu

on live.lean-lang.org

Additional Information

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Possibly related to #3219 or #5667