Zulip Chat Archive

Stream: general

Topic: Heavy refl

Yaël Dillies (Dec 09 2021 at 06:04):

I pushed the heavy refl on line 90 of algebra.category.Module.filtered_colimits over the boundary in branch#distrib_mul_action_with_zero (see https://github.com/leanprover-community/mathlib/runs/4396819546?check_suite_focus=true). I managed to solve it by adding a dsimp, but maybe people can speed up more.

Yaël Dillies (Dec 11 2021 at 09:14):

And it just bites me again, even with the dsimp. Can anyone speed it up?

Last updated: Dec 20 2023 at 11:08 UTC