Porting note: `simp` / `@[simp]` can prove it

[pitmonticone]

Classifies porting notes claiming anything semantically equivalent to

• "simp can prove this"
• "simp can simplify this`"
• "was @[simp], now can be proved by simp"
• "was @[simp], but simp can prove it"
• "removed simp attribute as the equality can already be obtained by simp"
• "simp can already prove this"
• "simp already proves this"
• "simp can prove these"
• "@[simp] can prove it"
• "@[simp] can prove this"

Related to: #11119

Examples

https://github.com/leanprover-community/mathlib4/blob/4b36afcf085586739aa4e59d507a7d01d9a2dbbf/Mathlib/Algebra/AddTorsor.lean#L194-L198

https://github.com/leanprover-community/mathlib4/blob/4b36afcf085586739aa4e59d507a7d01d9a2dbbf/Mathlib/Algebra/CubicDiscriminant.lean#L236-L239

https://github.com/leanprover-community/mathlib4/blob/4b36afcf085586739aa4e59d507a7d01d9a2dbbf/Mathlib/Algebra/Module/Basic.lean#L257-L260

https://github.com/leanprover-community/mathlib4/blob/76e9597c4920fd0421f70311e28cfc396367a5d1/Mathlib/Algebra/GCDMonoid/Basic.lean#L136-L146

[pitmonticone]

Regarding these porting note

https://github.com/leanprover-community/mathlib4/blob/4b36afcf085586739aa4e59d507a7d01d9a2dbbf/Mathlib/CategoryTheory/Limits/IsLimit.lean#L571

@kbuzzard said:

What is going on with this one? Is this a bug in the simpNF linter?

[pitmonticone]

Regarding these porting note

https://github.com/leanprover-community/mathlib4/blob/4b36afcf085586739aa4e59d507a7d01d9a2dbbf/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean#L261

@kbuzzard said:

What is going on with this one?

[pitmonticone]

Regarding these porting note

https://github.com/leanprover-community/mathlib4/blob/4b36afcf085586739aa4e59d507a7d01d9a2dbbf/Mathlib/Data/Vector.lean#L249

@kbuzzard said:

Is this the correct solution for this problem?