feat: more sub lemmas for Nat

[fgdorais]

• Mathlib patch: [Merged by Bors] - fix: patch for std4#203 (more sub lemmas for Nat) mathlib4#6216

There's a bunch of deprecated lemmas, all of which have better alternatives except for one which appears to be a single purpose lemma that lost its purpose.

[semorrison]

@YaelDillies, do you have an opinion here, or are able to review?

[fgdorais]

This is the last in a series. They're mostly independent but it might be easier to start with #194.

[YaelDillies]

I'm happy with the deprecations. However I find it a bit sad to duplicate all this tsub material in Std. Can we do some subset of the following suggestions?

• Not duplicate tsub lemma in Std
• Put in the docstring of duplicate Nat.sub_something that tsub_something exists in mathlib
• Deprecate mathlib-wise (is that currently possible?) each Nat.sub_something in favor of tsub_something
• Put a big warning in Std.Data.Nat.Lemmas that if people want a lot of theory about truncated subtraction, then they should use Mathlib.Algebra.Order.Sub.Canonical instead of PRing more lemmas here

[digama0]

I'd rather we did none of the above. The tsub lemmas are more complex to understand, and elaborate. I think there should be no particular preference in mathlib for one over the other. Certainly there won't be a warning about not adding any more lemmas on Nat: tsub is only relevant if you care about other types with truncated subtraction like NNReal, and for a lot of users of Std that's just not relevant, while Nat is very relevant.

[YaelDillies]

If we had to only do one of my suggestions, I would like it to be

• Put in the docstring of duplicate Nat.sub_something that tsub_something exists in mathlib

because I want mathlib users to be directed towards the API that's useful to them, avoiding ad hoc Std lemmas.

[fgdorais]

@YaelDillies Note that Nat lemmas in Std are primarily to reason about sizes of objects, array indices and such. There's no intent to duplicate or clash with Mathlib. My impression is that most users would use these lemmas for their intended purpose, so I don't quite see the need for the first three suggestions.

However, I am happy with the fourth suggestion:

• Put a big warning in Std.Data.Nat.Lemmas that if people want a lot of theory about truncated subtraction, then they should use Mathlib.Algebra.Order.Sub.Canonical instead of PRing more lemmas here

I will add a module doc to clarify the intended purpose of these lemmas and a pointer to Mathlib alternatives.

I would like to hear what others think before implementing the first three suggestions.

[fgdorais]

@YaelDillies Please see #237.

[semorrison]

I agree that module-docs are the way to go to explain the additional theory available in Mathlib.

Any results that are needed or helpful for non-mathematical uses of Nat need to be here in Std, without expecting such users to know about the general theory of truncated subtraction.

I am ambivalent about the "Mathlib-specific deprecation" suggestion, but don't think we should mention tsub in Std.

@fgdorais, as far as I'm concerned I think you can mark this back as awaiting-review.

[digama0]

Approved with modification:

• succ_sub_one, sub_lt_self, sub_one_sub_lt were undeprecated
• deprecated theorems were moved after their respective undeprecated versions instead of in a separate section (if we want this it should be implemented in docgen)

[semorrison]

Looks good to me. @digama0 has already approved, and @fgdorais has resolved the merge conflicts, so I hope we can merge this round!!