mathlib3

fd45e288 - fix(*): do not nolint simp_nf (#2734)

fix(*): do not nolint simp_nf (#2734) 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.