mathlib3

d79105ef - feat(tactic/field_simp): let field_simp use norm_num to prove numerals are nonzero (#5418)

feat(tactic/field_simp): let field_simp use norm_num to prove numerals are nonzero (#5418) As suggested by @robertylewis in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Solving.20simple.20%28in%29equalities.20gets.20frustrating/near/220278546, change the discharger in `field_simp` to try `assumption` on goals `x ≠ 0` and `norm_num1` on these goals when `x` is a numeral.