feat(algebra/ne_zero): generalize lemmas (#17477)
Lemmas with reduced typeclass assumptions:
`zero_ne_one` `one_ne_zero` `two_ne_zero` `three_ne_zero` `four_ne_zero` `ne_zero_of_eq_one`
Removed lemmas:
`is_R_or_C.two_ne_zero` `two_ne_zero'`
New explicit version lemmas:
`zero_ne_one'` `one_ne_zero'` `two_ne_zero'` `three_ne_zero'` `four_ne_zero'`
Renamed lemma:
`ne_zero.ne'` -> `ne_zero.nat_cast_ne`
New lemma:
`ne_zero.ne'`
Most of other diffs are just simply replace `@lemma` with new explicit lemmas
mathlib4: https://github.com/leanprover-community/mathlib4/pull/577
