feat(tactic/lint): check for redundant simp lemmas (#2066)

* chore(*): fix simp lemmas

* feat(tactic/lint): check for redundant simp lemmas

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Author: gebner

docs/commands.md

@@ -116,7 +116,7 @@ The following linters are run by default:
 9.  `incorrect_type_class_argument` checks for arguments in [square brackets] that are not classes.
 10. `dangerous_instance` checks for instances that generate type-class problems with metavariables.
 11. `inhabited_nonempty` checks for `inhabited` instance arguments that should be changed to `nonempty`.
-12. `simp_nf` checks that arguments of the left-hand side of simp lemmas are in simp-normal form.
+12. `simp_nf` checks that the left-hand side of simp lemmas is in simp-normal form.
 13. `simp_var_head` checks that there are no variables as head symbol of left-hand sides of simp lemmas.
 14. `simp_comm` checks that no commutativity lemmas (such as `add_comm`) are marked simp.
 

src/algebra/associated.lean

@@ -49,8 +49,8 @@ by rw [mul_comm, mul_dvd_of_is_unit_left h]
 @[simp] lemma unit_mul_dvd_iff [comm_semiring α] {a b : α} {u : units α} : (u : α) * a ∣ b ↔ a ∣ b :=
 mul_dvd_of_is_unit_left (is_unit_unit _)
 
-@[simp] lemma mul_unit_dvd_iff [comm_semiring α] {a b : α} {u : units α} : a * u ∣ b ↔ a ∣ b :=
-mul_dvd_of_is_unit_right (is_unit_unit _)
+lemma mul_unit_dvd_iff [comm_semiring α] {a b : α} {u : units α} : a * u ∣ b ↔ a ∣ b :=
+units.coe_mul_dvd _ _ _
 
 theorem is_unit_of_dvd_unit {α} [comm_semiring α] {x y : α}
   (xy : x ∣ y) (hu : is_unit y) : is_unit x :=
@@ -258,9 +258,8 @@ multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.not_unit])
 lemma dvd_iff_dvd_of_rel_left [comm_semiring α] {a b c : α} (h : a ~ᵤ b) : a ∣ c ↔ b ∣ c :=
 let ⟨u, hu⟩ := h in hu ▸ mul_unit_dvd_iff.symm
 
-@[simp] lemma dvd_mul_unit_iff [comm_semiring α] {a b : α} {u : units α} : a ∣ b * u ↔ a ∣ b :=
-⟨λ ⟨d, hd⟩, ⟨d * (u⁻¹ : units α), by simp [(mul_assoc _ _ _).symm, hd.symm]⟩,
-  λ h, dvd.trans h (by simp)⟩
+lemma dvd_mul_unit_iff [comm_semiring α] {a b : α} {u : units α} : a ∣ b * u ↔ a ∣ b :=
+units.dvd_coe_mul _ _ _
 
 lemma dvd_iff_dvd_of_rel_right [comm_semiring α] {a b c : α} (h : b ~ᵤ c) : a ∣ b ↔ a ∣ c :=
 let ⟨u, hu⟩ := h in hu ▸ dvd_mul_unit_iff.symm

src/algebra/big_operators.lean

@@ -55,9 +55,10 @@ lemma prod_pair [decidable_eq α] {a b : α} (h : a ≠ b) :
   ({a, b} : finset α).prod f = f a * f b :=
 by simp [prod_insert (not_mem_singleton.2 h.symm), mul_comm]
 
-@[simp] lemma prod_const_one : s.prod (λx, (1 : β)) = 1 :=
+@[simp, priority 1100] lemma prod_const_one : s.prod (λx, (1 : β)) = 1 :=
 by simp only [finset.prod, multiset.map_const, multiset.prod_repeat, one_pow]
-@[simp] lemma sum_const_zero {β} {s : finset α} [add_comm_monoid β] : s.sum (λx, (0 : β)) = 0 :=
+@[simp, priority 1100] lemma sum_const_zero {β} {s : finset α} [add_comm_monoid β] :
+  s.sum (λx, (0 : β)) = 0 :=
 @prod_const_one _ (multiplicative β) _ _
 attribute [to_additive] prod_const_one
 

src/algebra/category/Group.lean

@@ -103,7 +103,7 @@ def mul_equiv.to_Group_iso [group X] [group Y] (e : X ≃* Y) : Group.of X ≅ G
 attribute [simps] mul_equiv.to_Group_iso add_equiv.to_AddGroup_iso
 
 /-- Build an isomorphism in the category `CommGroup` from a `mul_equiv` between `comm_group`s. -/
-@[simps, to_additive add_equiv.to_AddCommGroup_iso "Build an isomorphism in the category `AddCommGroup` from a `add_equiv` between `add_comm_group`s."]
+@[to_additive add_equiv.to_AddCommGroup_iso "Build an isomorphism in the category `AddCommGroup` from a `add_equiv` between `add_comm_group`s."]
 def mul_equiv.to_CommGroup_iso [comm_group X] [comm_group Y] (e : X ≃* Y) : CommGroup.of X ≅ CommGroup.of Y :=
 { hom := e.to_monoid_hom,
   inv := e.symm.to_monoid_hom }

src/algebra/char_zero.lean

@@ -55,7 +55,7 @@ cast_injective.eq_iff
 @[simp, elim_cast] theorem cast_eq_zero {n : ℕ} : (n : α) = 0 ↔ n = 0 :=
 by rw [← cast_zero, cast_inj]
 
-@[simp, elim_cast] theorem cast_ne_zero {n : ℕ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
+@[elim_cast] theorem cast_ne_zero {n : ℕ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
 not_congr cast_eq_zero
 
 end nat

src/algebra/commute.lean

@@ -82,13 +82,13 @@ variables {M : Type*} [monoid M]
 @[simp] theorem one_right (a : M) : commute a 1 := semiconj_by.one_right a
 @[simp] theorem one_left (a : M) : commute 1 a := semiconj_by.one_left a
 
-@[simp] theorem units_inv_right {a : M} {u : units M} : commute a u → commute a ↑u⁻¹ :=
+theorem units_inv_right {a : M} {u : units M} : commute a u → commute a ↑u⁻¹ :=
 semiconj_by.units_inv_right
 
 @[simp] theorem units_inv_right_iff {a : M} {u : units M} : commute a ↑u⁻¹ ↔ commute a u :=
 semiconj_by.units_inv_right_iff
 
-@[simp] theorem units_inv_left {u : units M} {a : M} : commute ↑u a → commute ↑u⁻¹ a :=
+theorem units_inv_left {u : units M} {a : M} : commute ↑u a → commute ↑u⁻¹ a :=
 semiconj_by.units_inv_symm_left
 
 @[simp] theorem units_inv_left_iff {u : units M} {a : M}: commute ↑u⁻¹ a ↔ commute ↑u a :=
@@ -122,10 +122,10 @@ section group
 
 variables {G : Type*} [group G] {a b : G}
 
-@[simp] theorem inv_right : commute a b → commute a b⁻¹ := semiconj_by.inv_right
+theorem inv_right : commute a b → commute a b⁻¹ := semiconj_by.inv_right
 @[simp] theorem inv_right_iff : commute a b⁻¹ ↔ commute a b := semiconj_by.inv_right_iff
 
-@[simp] theorem inv_left :  commute a b → commute a⁻¹ b := semiconj_by.inv_symm_left
+theorem inv_left :  commute a b → commute a⁻¹ b := semiconj_by.inv_symm_left
 @[simp] theorem inv_left_iff : commute a⁻¹ b ↔ commute a b := semiconj_by.inv_symm_left_iff
 
 theorem inv_inv : commute a b → commute a⁻¹ b⁻¹ := semiconj_by.inv_inv_symm
@@ -186,10 +186,10 @@ section ring
 
 variables {R : Type*} [ring R] {a b c : R}
 
-@[simp] theorem neg_right : commute a b → commute a (- b) := semiconj_by.neg_right
+theorem neg_right : commute a b → commute a (- b) := semiconj_by.neg_right
 @[simp] theorem neg_right_iff : commute a (-b) ↔ commute a b := semiconj_by.neg_right_iff
 
-@[simp] theorem neg_left : commute a b → commute (- a) b := semiconj_by.neg_left
+theorem neg_left : commute a b → commute (- a) b := semiconj_by.neg_left
 @[simp] theorem neg_left_iff : commute (-a) b ↔ commute a b := semiconj_by.neg_left_iff
 
 @[simp] theorem neg_one_right (a : R) : commute a (-1) := semiconj_by.neg_one_right a

src/algebra/free.lean

@@ -252,7 +252,7 @@ def lift (x : free_semigroup α) : β :=
 lift' f x.1 x.2
 
 @[simp] lemma lift_of (x : α) : lift f (of x) = f x := rfl
-@[simp] lemma lift_of_mul (x y) : lift f (of x * y) = f x * lift f y := rfl
+lemma lift_of_mul (x y) : lift f (of x * y) = f x * lift f y := rfl
 
 @[simp] lemma lift_mul (x y) : lift f (x * y) = lift f x * lift f y :=
 free_semigroup.induction_on x (λ p, rfl)

src/algebra/group/basic.lean

@@ -60,15 +60,15 @@ theorem mul_right_surjective (a : G) : function.surjective (λ x, x * a) :=
 theorem eq_of_inv_eq_inv : a⁻¹ = b⁻¹ → a = b :=
 inv_inj'.1
 
-@[simp, to_additive]
+@[to_additive]
 theorem mul_self_iff_eq_one : a * a = a ↔ a = 1 :=
 by have := @mul_left_inj _ _ a a 1; rwa mul_one at this
 
 @[simp, to_additive]
 theorem inv_eq_one : a⁻¹ = 1 ↔ a = 1 :=
 by rw [← @inv_inj' _ _ a 1, one_inv]
 
-@[simp, to_additive]
+@[to_additive]
 theorem inv_ne_one : a⁻¹ ≠ 1 ↔ a ≠ 1 :=
 not_congr inv_eq_one
 

src/algebra/group_power.lean

@@ -98,9 +98,11 @@ by rw [←pow_add, ←pow_add, add_comm]
 theorem smul_add_comm : ∀ (a : A) (m n : ℕ), m•a + n•a = n•a + m•a :=
 @pow_mul_comm (multiplicative A) _
 
-@[simp] theorem list.prod_repeat (a : M) (n : ℕ) : (list.repeat a n).prod = a ^ n :=
+@[simp, priority 500]
+theorem list.prod_repeat (a : M) (n : ℕ) : (list.repeat a n).prod = a ^ n :=
 by induction n with n ih; [refl, rw [list.repeat_succ, list.prod_cons, ih]]; refl
-@[simp] theorem list.sum_repeat : ∀ (a : A) (n : ℕ), (list.repeat a n).sum = n • a :=
+@[simp, priority 500]
+theorem list.sum_repeat : ∀ (a : A) (n : ℕ), (list.repeat a n).sum = n • a :=
 @list.prod_repeat (multiplicative A) _
 
 theorem monoid_hom.map_pow (f : M →* N) (a : M) : ∀(n : ℕ), f (a ^ n) = (f a) ^ n

src/algebra/lie_algebra.lean

@@ -191,10 +191,14 @@ instance (R : Type u) (L : Type v) (L' : Type v)
   [comm_ring R] [add_comm_group L] [lie_algebra R L] [add_comm_group L'] [lie_algebra R L'] :
   has_coe (L →ₗ⁅R⁆ L') (L →ₗ[R] L') := ⟨morphism.to_linear_map⟩
 
-@[simp] lemma map_lie {R : Type u} {L : Type v} {L' : Type v}
+lemma map_lie {R : Type u} {L : Type v} {L' : Type v}
   [comm_ring R] [add_comm_group L] [lie_algebra R L] [add_comm_group L'] [lie_algebra R L']
   (f : L →ₗ⁅R⁆ L') (x y : L) : f ⁅x, y⁆ = ⁅f x, f y⁆ := morphism.map_lie f
 
+@[simp] lemma map_lie' {R : Type u} {L : Type v} {L' : Type v}
+  [comm_ring R] [add_comm_group L] [lie_algebra R L] [add_comm_group L'] [lie_algebra R L']
+  (f : L →ₗ⁅R⁆ L') (x y : L) : (f : L →ₗ[R] L') ⁅x, y⁆ = ⁅f x, f y⁆ := morphism.map_lie f
+
 variables {R : Type u} {L : Type v} [comm_ring R] [add_comm_group L] [lie_algebra R L]
 
 /--