[Merged by Bors] - fix(*): do not nolint simp_nf

[gebner]

The nolint simp_nf for subgroup.coe_coe was hiding an actual nontermination issue. Please just ping me if you're unsure about the simp_nf linter.

[bryangingechen]

@digama0 and I discussed some related simp_nf lints briefly here.

Since this PR removes the division_ring versions of inv_zero and div_zero, should we also remove the previously-discussed inv_one, div_one, zero_div and inv_inv' from algebra.field?

[gebner]

Ok, I missed the discussion. There was just too much going on on zulip.

should we also remove the previously-discussed inv_one, div_one, zero_div and inv_inv' from algebra.field?

I think so but maybe in another PR. There's a lot of lemmas in group_with_zero that we could unprime.

The message doesn't give any hints as to which lemma is bad

@digama0 Do you remember what this was about? The linter output clearly calls out both lemmas involved in the issue:

#print inv_one /- simp can prove this:
  by simp only [inv_one']
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].
 -/

[robertylewis]

I think this is a good change and as Gabriel says, more unpriming can happen later.

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs