PR !4#1470: feat: `attach` and `filter` lemmas

Stream: triage

[Random Issue Bot]

Today I chose PR 1470 for discussion!

feat: attach and filter lemmas
Created by @Yaël Dillies (@YaelDillies) on 2023-01-10
Labels: awaiting-author, mathlib3-pair, forward-port-placeholder

Is this PR still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

Still waiting on !3#18087

[Kevin Buzzard]

Explain again why we are ever waiting for mathlib3 for anything now?

[Ruben Van de Velde]

So Yaël doesn't need to port the code by hand (if ever a mathlib3 reviewer stands up)

[Yaël Dillies]

I mean, it's not even like it's unreviewed. It's been LGTM for a month and a half.

[Johan Commelin]

cc @Eric Wieser

[Patrick Massot]

What about forgetting about Lean 3 and moving on?

[Johan Commelin]

Ooh, in cases like this I can imagine that it's nice to have help from mathport automation.

[Eric Wieser]

#outofsync is still pretty long, I think review time is better spent there than on mathlib3 PRs

[Yaël Dillies]

Johan is exactly right. I've been oneshotting my self-contained PRs and branches, but the ones that span several files are a pain to do by hand.