push_neg user command

Stream: metaprogramming / tactics

[Heather Macbeth]

I have written (#16775) a user command for push_neg, so that one can type

#push_neg ¬(∃ x : ℝ, ∀ y, x < y → x = 3)

and see output in the infoview

∀ (x : ℝ), ∃ (y : ℝ), x < y ∧ x ≠ 3

I expect to use this for teaching, and maybe others will too.

[Heather Macbeth]

The code is copied blindly from #simp and #norm_num so it could use a careful review.

[Kyle Miller]

I made #norm_num by copying blindly from #simp, so I'll take a look :smile: