change filter inf #8657

Stream: PR reviews

[Patrick Massot]

@Sebastien Gouezel and @Yury G. Kudryashov I'm sorry I doubly messed up with #8657. I started a large refactor without warning and I got carried away and actually mixed three refactors. If you don't like it then I won't complain. But I'd be very grateful if you could merge it soon because it touches 88 files...

[Sebastien Gouezel]

88! :octopus:

[Anne Baanen]

185482642257398439114796845645546284380220968949399346684421580986889562184028199319100141244804501828416633516851200000000000000000000 :octopus:

[Yury G. Kudryashov]

Should I cherry-pick "rename lemmas" diff from your branch to a new PR to make things easier to review?

[Eric Wieser]

That seems sensible to me if you're happy to do it

[Patrick Massot]

I think it makes sense only if we decide we don't want to change the definition of filter.inf. Otherwise it's too much work for too little use.

[Eric Wieser]

An 88 file PR is pretty hard to review for interesting changes when most of the diff is just renames. The options then essentially become: 1) spend a really painful time looking for the relevant bits in review, 2) have Yury split the non-relevant rename bits into a new PR, if they're happy to do so. Then only one person has to work out which bits are relevent rather than every reviewer. 3) trust that the changes are ok without looking at all of them. I suspect Yury can do 2) quite quickly, but I agree it's not worth doing if no one wants to step up.

[Patrick Massot]

The linter says this change is great:

/- The `unused_arguments` linter reports: -/
/- UNUSED ARGUMENTS. -/
-- order/filter/basic.lean
#print filter.infi_sets_induct /- argument 9: (upw : ∀ {s₁ s₂ : set α}, s₁ ⊆ s₂ → p s₁ → p s₂) -/

A lemma became more powerful thanks to the new definition.

[Yury G. Kudryashov]

Golfed a few proofs. Looks good to me. Note that we should ban all other topology/analysis-related PRs from the merge queue while bors will work on this one.

[Patrick Massot]

I think the only contender right now is #8651 which seems fine.

[Patrick Massot]

Should I merge now?

[Patrick Massot]

Actually, it does conflict #8651, so let's wait.