Tactic Request: `nonzero`/`positivity` improvements

[BoltonBailey]

A nonzero tactic, as suggested by Yury: #general > "Missing Tactics" list @ 💬

• capable of proving example (a b : ℂ) (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 := by sorry (positivity fails with failed to synthesize PartialOrder ℂ)
• If this is to be distinct from positivity, let it be a discharger for field_simp.

Also potentially useful would be an attribute to automatically allow lemmas to be used by this or the positivity tactic simply by tagging them (I believe metaprogramming is needed to add a lemma currently).

[JovanGerb]

This improvement to positivity is now in mathlib, thanks to leanprover-community/mathlib4#35394

The idea of simply tagging lemmas with @[positivity] would still be useful though.

[BoltonBailey]

I was trying out the Claude Fable LLM to handle the attribute part of this in leanprover-community/mathlib4#41895 and I was a bit surprised to find that it fairly quickly made a version of it that allowed it to successfully golf away a lot of positivity extensions while still passing the positivity test suite.

[JovanGerb]

Having a quick look at the code in that PR, it looks quite LLMy - I'd rather have this implemented by a person. But it's nice to know that such an attribute is feasible.

[BoltonBailey]

Here's a relevant Zulip link (#general > "Missing Tactics" list @ 💬), hopefully it comes along soon!