Two other possibilities:

• reducible (not sure how much you have to make it though)
• { Con.monoid _ with } should do what you did manually

Two other possibilities:

• reducible (not sure how much you have to make it though)
• { Con.monoid _ with } should do what you did manually

{ Con.monoid _ with } doesn't do the same thing, because it doesn't use the existing MulOneClass instance to fill in the Mul and One fields, so you still have to unfold Con.monoid to check the defeq. This approach does not fix the simp failure.
I think Con.monoid should already be reducible since it's an instance.

It looks like leanprover/lean4#2478 will fix the timeouts in #6803 without modifying the instance (it was probably unifying against something that was improperly unfolded to start with). There is #7257 to test out yourself in case I merged something oddly.

I did try merging my amalgamated products PR into #7257. It seemed to fix the timeout at the end, but not the simp failure nearer the start of the file. It still failed to simplify inl 1 to 1.

bors r+

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style