Golf a few proofs

[pitmonticone]

No description provided.

[alma-n]

Thanks for the changes. We will look at them in more detail at a later date. Could you possibly add some explanations regarding the changes you made? As an example specifically: Why use refine over intro and apply?

[pitmonticone]

Hi @alma-n, these changes have been made to:

• Simplify proofs
• Reduce the number of lines of code
• Enhance readability of some proofs by using · to indent multiple cases
• Replace induction' (which will soon be deprecated) with induction
• Favour proof terms over tactics for quick one-liners
• Avoid intermediate simp by using simp only if preceding a rigid-input tactic such as apply, exact, rw, etc.

Why use refine over intro and apply?

I have used refine only once just to reduce lines of code. Not a major improvement in that case.

[YaelDillies]

Replace induction' (which will soon be deprecated) with induction

Where did you get that from? I think there's enough people liking induction' over induction that it still has a long life ahead.

[pitmonticone]

In multiple Mathlib PR reviews, I have been advised to replace induction' with induction due to its "suboptimal" status or impending removal, as noted by maintainers such as @sgouezel (for instance, see this discussion).

I'm sorry if I misinterpreted those review comments. However, given these recommendations in Mathlib PRs, I thought it would have been prudent to also suggest this as a best practice for external projects like this one.