further reading on transitioning from `extra` to `positivity` tactic

[rzeta0]

I'm aware that some of the tactics in this course are specifically created by you to aid learning - thank you!

I'm trying to create a small task and proof which uses the idea of a squared number being positive, and trying to create an educational example using vanilla lean4/mathlib. I think that means using the positivity tactic.

I'm not succeeding and I can't seem to find examples / guides online despite trying hard. I can't even find a good example of positivity, the examples in the lean3 docs are too small ( https://leanprover-community.github.io/mathlib_docs/tactics.html#positivity ).

Can you point us to some notes / guidance on how to use positivity?

The lean zulip chat hasn't been helpful on this matter, except to point out that in a calc proof a line must have the form 0 < x which adds an extra challenge.

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/example.20of.20.60positivity.60.20tactic

---

Here is the example I'm trying to develop - essentially to say that if c^2 = a^2 + b^2 then c^2 >= a^2.

import Mathlib.Tactic

example {a b : ℤ} (h1 : a^2 + b^2 = c^2) : 0 ≤ c^2 - a^2 :=
  calc
    0 = c^2 - a^2 - b^2 := by linarith [h1]
    _ ≤ c^2 - a^2 := by positivity