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
|
-- 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 |
|
-- @[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' |
|
-- 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 |
|
-- 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 |
Classifies porting notes claiming anything semantically equivalent to
simpcan prove this"simpcan simplify this`"@[simp], now can be proved bysimp"@[simp], butsimpcan prove it"simp"simpcan already prove this"simpalready proves this"simpcan prove these"Related to: #11119
Examples
mathlib4/Mathlib/Algebra/AddTorsor.lean
Lines 194 to 198 in 4b36afc
mathlib4/Mathlib/Algebra/CubicDiscriminant.lean
Lines 236 to 239 in 4b36afc
mathlib4/Mathlib/Algebra/Module/Basic.lean
Lines 257 to 260 in 4b36afc
mathlib4/Mathlib/Algebra/GCDMonoid/Basic.lean
Lines 136 to 146 in 76e9597