Yury G. Kudryashov
Yury G. Kudryashov
I cherry-picked parts about `WithTop`/`WithBot`-based types to #13264
@FR-vdash-bot What parts of this is not in `master` yet? Do you need help with merging `master`?
Let me repeat my concern from Lean3 PR: > Note that if we go forward with this refactor, the monoid structure on `CategoryTheory.End (GroupCat.of G)` will be no longer defeq...
`Monoid (CategoryTheory.End _)` is defined uniformly for all categories, you can't fix `pow` for one category. If you want to be able to do that, then you need to include...
The issue is not about translation. The issue is that we'll have 2 defeq types (`X --> X` for some categories) with propeq but not defeq instances about them.
Could you please open a Zulip discussion? I don't want to merge this PR myself, but if another maintainer rules my objection as invalid/irrelevant, then I won't insist.
Is it from an open source project? If yes, then please link. Also, what do you think about adding these generic lemmas? ``` namespace List variable {α M : Type*}...
I missed that discussion, found and added a link.
I don't think that adding lemmas is a right way to deal with `exact?` being unable to use `trans_le`. IMHO, we should resurrect a tactic for proving inequalities using chains...
I'm changing it to `awaiting-author` because it's marked as a draft PR and as a `WIP`. If it's ready for review, then please change it from draft to a normal...