changelog-library

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d538e1cd90bc8dce3e8919d2ed496903577a63a9 --onto 7bfa8f6296ebfebc497d5b30d34f494bcc9782a2. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-10 23:27:54)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d538e1cd90bc8dce3e8919d2ed496903577a63a9 --onto 8fc8e8ed19ef218022f5a94cbf5e472e3b777e44. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-11 23:03:09)

Should we worry about this having a rather unspecific simp discrimination tree key? Or is it worthy trying this on every forIn loop?

The existing lemmas already have this problem:

import Lean

/--
info: @Eq
  _
  (@forIn' _ (List _) _ _ _ _ _ _ _ <other>)
  (@List.foldlM _ _ _ (@Subtype _ (@Membership.mem _ (List _) _ _)) <other> _ (@List.attach _ _))
-/
#guard_msgs in
#discr_tree_key List.forIn'_yield_eq_foldlM -- already `simp`

/--
info: @Eq
  _
  (@forIn' _ (List _) _ _ _ _ _ _ _ <other>)
  (@pure _ _ _ (@List.foldl _ (@Subtype _ (@Membership.mem _ (List _) _ _)) <other> _ (@List.attach _ _)))
-/
#guard_msgs in
#discr_tree_key List.forIn'_pure_yield_eq_foldl -- `simp` in this PR

Thanks for checking