nightly-2025-11-20 grind behavior on dependent pairs

Stream: lean4

[Chris Henson]

On v4.26.0-rc1 the destructuring below the comment can be removed, but causes grind to fail on nightly-2025-11-20:

@[grind =]
def List.map_snd (f : β → β) (xs : List ((_ : α) × β)) : List ((_ : α) × β) :=
  xs.map (fun ⟨a,b⟩ => ⟨a, f b⟩)

theorem List.map_snd_id (xs : List ((_ : α) × β)) : xs.map_snd id = xs := by
  induction xs with
  | nil => grind
  | cons hd =>
      -- removing this works on `v4.26.0-rc1`, but fails on `nightly-2025-11-20`
      let ⟨_, _⟩ := hd
      grind

[Chris Henson]

Using show_eqcs in the new interactive mode gives some info. On v4.26.0-rc1 we have

[eqc] Equivalence classes ▼
  [] {hd, ⟨hd.fst, hd.snd⟩}
  [] {tail✝, map_snd id tail✝}
  [] others ▼
    [] {hd.fst, ⟨hd.fst, hd.snd⟩.fst}
    [] {hd.snd, ⟨hd.fst, hd.snd⟩.snd}

at the beginning of the cons branch of the proof, while on nightly all of the classes related to projections are not present.

I tried to reproduce with something other than lists, but have not been successful so far.

[Kim Morrison]

Happily, it is working again on nightly-2025-11-23. There were a few bugfixes between those nightlies, but I am not sure which one was relevant!