Bryan Gin-ge Chen
Bryan Gin-ge Chen
It may be too late now, but I'm guessing we didn't intend to merge this with the RFC title as is?
It looks to me like the discussion on Zulip about whether `shake` should be in its own repository is still unresolved.
I ran into this in [`linear_algebra.basic`](https://github.com/leanprover-community/mathlib/blob/5169595d2d982ba522047b6709c112bf305f87d8/src/linear_algebra/basic.lean#L1345) and I just added a `nolint` attribute there.
bors r- Please merge `master`, fix the build and place back on the queue by commenting `bors merge`. Thanks!
The same thing happens for `remove_reaction` and probably some other methods as well; I believe the root cause is that the methods don't strip `message_id` from the data attached to...
OK, cool. That's encouraging! I'm not likely to be able to tackle this myself anytime soon though.
@cipher1024 notes [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Trouble.20with.20cases.20and.20rintro.20.2F.20rcases/near/215939792) that `field f1` works instead. Leaving this open for now since [the tactic doc entry](https://leanprover-community.github.io/mathlib_docs/tactics.html#refine_struct) doesn't mention this (and the (text mode) tactic state says `case`),...