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

mathlib4/Mathlib/Algebra/AddTorsor.lean

Lines 194 to 198 in 4b36afc

	-- Porting note: simp can prove this
	--@[simp]
	theorem singleton_vsub_self (p : P) : ({p} : Set P) -ᵥ {p} = {(0 : G)} := by
	rw [Set.singleton_vsub_singleton, vsub_self]
	#align set.singleton_vsub_self Set.singleton_vsub_self

mathlib4/Mathlib/Algebra/CubicDiscriminant.lean

Lines 236 to 239 in 4b36afc

	-- @[simp] -- Porting note: simp can prove this
	theorem leadingCoeff_of_c_eq_zero' : (toPoly ⟨0, 0, 0, d⟩).leadingCoeff = d :=
	leadingCoeff_of_c_eq_zero rfl rfl rfl
	#align cubic.leading_coeff_of_c_eq_zero' Cubic.leadingCoeff_of_c_eq_zero'

mathlib4/Mathlib/Algebra/Module/Basic.lean

Lines 257 to 260 in 4b36afc

	-- Porting note: simp can prove this
	--@[simp]
	theorem neg_smul_neg : -r • -x = r • x := by rw [neg_smul, smul_neg, neg_neg]
	#align neg_smul_neg neg_smul_neg

mathlib4/Mathlib/Algebra/GCDMonoid/Basic.lean

Lines 136 to 146 in 76e9597

	-- Porting note: `simp` can prove this
	-- @[simp]
	theorem normalize_zero : normalize (0 : α) = 0 :=
	normalize.map_zero
	#align normalize_zero normalize_zero
	-- Porting note: `simp` can prove this
	-- @[simp]
	theorem normalize_one : normalize (1 : α) = 1 :=
	normalize.map_one
	#align normalize_one normalize_one

[pitmonticone]

Regarding these porting note

mathlib4/Mathlib/CategoryTheory/Limits/IsLimit.lean

Line 571 in 4b36afc

-- Porting note: simp can prove this. Linter claims it still is tagged with simp

@kbuzzard said:

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

[pitmonticone]

Regarding these porting note

mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

Line 261 in 4b36afc

-- Porting note: simp can prove this, linter doesn't notice it is removed

@kbuzzard said:

What is going on with this one?

[pitmonticone]

Regarding these porting note

mathlib4/Mathlib/Data/Vector.lean

Line 249 in 4b36afc

@[simp, nolint simpNF] -- Porting note: simp can prove this in the future

@kbuzzard said:

Is this the correct solution for this problem?