chore: remove redundant LinearEquiv.map_neg/sub (#12330)

These are redundant with `_root_.{map_neg,map_sub}`.

Author: Ruben-VandeVelde

Mathlib/Algebra/Lie/Matrix.lean

@@ -45,7 +45,7 @@ def lieEquivMatrix' : Module.End R (n → R) ≃ₗ⁅R⁆ Matrix n n R :=
       let f := @LinearMap.toMatrix' R _ n n _ _
       change f (T.comp S - S.comp T) = f T * f S - f S * f T
       have h : ∀ T S : Module.End R _, f (T.comp S) = f T * f S := LinearMap.toMatrix'_comp
-      rw [LinearEquiv.map_sub, h, h] }
+      rw [map_sub, h, h] }
 #align lie_equiv_matrix' lieEquivMatrix'
 
 @[simp]

Mathlib/Algebra/Lie/OfAssociative.lean

@@ -377,7 +377,7 @@ def lieConj : Module.End R M₁ ≃ₗ⁅R⁆ Module.End R M₂ :=
     map_lie' := fun {f g} =>
       show e.conj ⁅f, g⁆ = ⁅e.conj f, e.conj g⁆ by
         simp only [LieRing.of_associative_ring_bracket, LinearMap.mul_eq_comp, e.conj_comp,
-          LinearEquiv.map_sub] }
+          map_sub] }
 #align linear_equiv.lie_conj LinearEquiv.lieConj
 
 @[simp]

Mathlib/Algebra/Module/Zlattice/Basic.lean

@@ -145,7 +145,7 @@ theorem fract_apply (m : E) : fract b m = m - floor b m := rfl
 
 @[simp]
 theorem repr_fract_apply (m : E) (i : ι) : b.repr (fract b m) i = Int.fract (b.repr m i) := by
-  rw [fract, LinearEquiv.map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.fract]
+  rw [fract, map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.fract]
 #align zspan.repr_fract_apply Zspan.repr_fract_apply
 
 @[simp]
@@ -195,7 +195,7 @@ theorem fract_eq_fract (m n : E) : fract b m = fract b n ↔ -m + n ∈ span ℤ
   classical
   rw [eq_comm, Basis.ext_elem_iff b]
   simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem,
-    sub_eq_neg_add, map_add, LinearEquiv.map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
+    sub_eq_neg_add, map_add, map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
     Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]
 #align zspan.fract_eq_fract Zspan.fract_eq_fract
 

Mathlib/LinearAlgebra/Basic.lean

@@ -532,15 +532,8 @@ variable {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPai
 variable {re₃₄ : RingHomInvPair σ₃₄ σ₄₃} {re₄₃ : RingHomInvPair σ₄₃ σ₃₄}
 variable (e e₁ : M ≃ₛₗ[σ₁₂] M₂) (e₂ : M₃ ≃ₛₗ[σ₃₄] M₄)
 
--- @[simp] -- Porting note (#10618): simp can prove this
-theorem map_neg (a : M) : e (-a) = -e a :=
-  e.toLinearMap.map_neg a
-#align linear_equiv.map_neg LinearEquiv.map_neg
-
--- @[simp] -- Porting note (#10618): simp can prove this
-theorem map_sub (a b : M) : e (a - b) = e a - e b :=
-  e.toLinearMap.map_sub a b
-#align linear_equiv.map_sub LinearEquiv.map_sub
+#align linear_equiv.map_neg map_negₓ
+#align linear_equiv.map_sub map_subₓ
 
 end AddCommGroup
 

Mathlib/LinearAlgebra/Basis.lean

@@ -1573,8 +1573,8 @@ theorem union_support_maximal_linearIndependent_eq_range_basis {ι : Type w} (b
       rw [← eq_neg_iff_add_eq_zero] at z
       replace z := neg_eq_iff_eq_neg.mpr z
       apply_fun fun x => b.repr x b' at z
-      simp only [repr_self, LinearEquiv.map_smul, mul_one, Finsupp.single_eq_same, Pi.neg_apply,
-        Finsupp.smul_single', LinearEquiv.map_neg, Finsupp.coe_neg] at z
+      simp only [repr_self, map_smul, mul_one, Finsupp.single_eq_same, Pi.neg_apply,
+        Finsupp.smul_single', map_neg, Finsupp.coe_neg] at z
       erw [DFunLike.congr_fun (Finsupp.apply_total R (b.repr : M →ₗ[R] ι →₀ R) v l.some) b'] at z
       simpa [Finsupp.total_apply, w] using z
     -- Then all the other coefficients are zero, because `v` is linear independent.

Mathlib/NumberTheory/ClassNumber/Finite.lean

@@ -246,7 +246,7 @@ theorem exists_mem_finsetApprox (a : S) {b} (hb : b ≠ (0 : R)) :
   refine' Int.cast_lt.mp ((norm_lt abv bS _ fun i => lt_of_le_of_lt _ (hjk' i)).trans_le _)
   · apply le_of_eq
     congr
-    simp_rw [map_sum, LinearEquiv.map_sub, LinearEquiv.map_smul, Finset.sum_apply',
+    simp_rw [map_sum, map_sub, map_smul, Finset.sum_apply',
       Finsupp.sub_apply, Finsupp.smul_apply, Finset.sum_sub_distrib, Basis.repr_self_apply,
       smul_eq_mul, mul_boole, Finset.sum_ite_eq', Finset.mem_univ, if_true]
   · exact mod_cast ε_le