Commit 2020-12-20 11:33 d79105ef

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.