[Merged by Bors] - feat(Finset): add gcongr attributes
#9520
Conversation
| theorem filter_subset_filter {s t : Finset α} (h : s ⊆ t) : s.filter p ⊆ t.filter p := fun _a ha => | ||
| mem_filter.2 ⟨h (mem_filter.1 ha).1, (mem_filter.1 ha).2⟩ | ||
| #align finset.filter_subset_filter Finset.filter_subset_filter | ||
|
|
||
| theorem monotone_filter_left : Monotone (filter p) := fun _ _ => filter_subset_filter p | ||
| #align finset.monotone_filter_left Finset.monotone_filter_left | ||
|
|
||
| -- TODO: `@[gcongr]` doesn't accept this lemma because of the `DecidablePred` arguments | ||
| theorem monotone_filter_right (s : Finset α) ⦃p q : α → Prop⦄ [DecidablePred p] [DecidablePred q] |
There was a problem hiding this comment.
This is interesting, I forgot we had this order on Prop. I wonder if there's a reimplementation of grw which exploits this more seriously.
If you want to make it gcongr, should we make a copy of this lemmas which uses classical reasoning and omits the [DecidablePred] hypotheses? (Would that work?)
There was a problem hiding this comment.
I guess, this would work but only if we're dealing with classical DecidablePreds in Finset.filter.
| simp only -- Need to unfold `xs` and do alpha reduction, otherwise `gcongr` fails | ||
| gcongr | ||
| refine ⟨xs, h_mono, tendsto_atTop_mono (fun n ↦ Finset.le_sup' _ ?_) h⟩ | ||
| simp |
I think these would all be reasonable. ( |
|
LGTM maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by jcommelin. |
| @@ -1135,6 +1143,12 @@ theorem inf'_mono {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonem | |||
| s₂.inf' (h₁.mono h) f ≤ s₁.inf' h₁ f := | |||
| Finset.le_inf' h₁ _ (fun _ hb => inf'_le _ (h hb)) | |||
|
|
|||
| /-- A version of `Finset.inf'_mono` acceptable for `@[gcongr]`. -/ | |||
There was a problem hiding this comment.
I don't remember what I wrote here precisely, probably it was asking for slightly more explanation which changes were needed: is it just that h₂ is added or also that h₁ and h₂ are marked as implicit now?
|
Not sure why I wanted to await-author here, I think with a comment we can be done. bors d+ |
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
Co-authored-by: Johan Commelin <johan@commelin.net>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
gcongr attributesgcongr attributes
I accidentally merged #9520 before pushing these changes requested by @Vierkantor
Co-authored-by: Johan Commelin <johan@commelin.net>
I accidentally merged #9520 before pushing these changes requested by @Vierkantor
Co-authored-by: Johan Commelin <johan@commelin.net>
I accidentally merged #9520 before pushing these changes requested by @Vierkantor
Co-authored-by: Johan Commelin <johan@commelin.net>
I accidentally merged #9520 before pushing these changes requested by @Vierkantor
Co-authored-by: Johan Commelin <johan@commelin.net>
I accidentally merged #9520 before pushing these changes requested by @Vierkantor
Co-authored-by: Johan Commelin <johan@commelin.net>
I accidentally merged #9520 before pushing these changes requested by @Vierkantor
@hrmacbeth In some cases I had to add equivalent lemmas to make
@[gcongr]happy.Should it accept
ifflemmas and/orMonotone/Antitone/StrictMono/StrictAntilemmas or it's hard to implement without hitting performance?