Anne Baanen

Or even, bors r+

Could you list the following things in the PR description: * Declarations that have been renamed * Declarations that have been changed (ignoring generalization of instance parameters, e.g. `boolean_algebra` to...

I think we will need to add a new case to `tactic.norm_num.eval_finset` to handle `univ : finset (fin n)`. Let me know if you're having trouble with that.

I don't think so, the case for `univ` just opens up the `fintype` instance and goes in recursion on the expression it finds in the `fintype.elems` field.

I've pushed a commit that should work, but we'll have to wait for all the dependencies of the test to build to find out.

Sorry, this dropped off my radar. Now it works! (for the one test file, on my machine...)

Okay: #15840.

bors d=@alexjbest

> BTW, why most lemmas take `(h : is_maximal _)`, not `[is_maximal _]`? I believe this is only a class to allow `R / I` to have a `field` instance...

It feels like the proof of `eq_zero_of_mul_eq_zero_of_smul` is slightly too complicated, but I can't figure out a way to simplify it (reordering proofs, trying `calc` blocks, etc.) So looks good...