Something like List.forall_unattach

Stream: Is there code for X?

[Will Bradley]

Would it be helpful if I added this lemma to Mathlib?

lemma List.forall_unattach {α: Type u} {p: α → Prop} {l: List { x // p x }}: ∀ x ∈ l.unattach, p x := by
  simp [List.unattach, -List.map_subtype]
  intros
  assumption

Or does it already exist somewhere under a different name?

[Kim Morrison]

Doesn't seem unreasonable. When I introduced unattach, however, I was hoping that people wouldn't use it! It's meant to be an intermediate form that is always simplified away.

[Kim Morrison]

May we need more vigorous warnings in the doc-strings...

[Martin Dvořák]

BTW try simp? so that you can replace the nonterminal simp by something more concrete.