chore(linear_algebra/alternating): golf a proof (#5666)

`sign_mul` seems to have been marked `simp` recently, making it not necessary to include in `simp` calls.

src/linear_algebra/alternating.lean

@@ -370,14 +370,7 @@ begin
   rw sum_apply,
   exact finset.sum_involution
     (λ σ _, swap i j * σ)
-    (λ σ _, begin
-      convert add_right_neg (↑σ.sign • m.dom_dom_congr σ v),
-      rw [perm.sign_mul, perm.sign_swap i_ne_j, ←neg_smul, smul_apply,
-        dom_dom_congr_apply, dom_dom_congr_apply],
-      congr' 2,
-      { simp },
-      { ext, simp [apply_swap_eq_self hv] },
-    end)
+    (λ σ _, by simp [perm.sign_swap i_ne_j, apply_swap_eq_self hv])
     (λ σ _ _, (not_congr swap_mul_eq_iff).mpr i_ne_j)
     (λ σ _, finset.mem_univ _)
     (λ σ _, swap_mul_involutive i j σ)

src/linear_algebra/determinant.lean

@@ -66,7 +66,7 @@ begin
           (by simp [apply_swap_eq_self hpij])
           (λ _ _ _ _ h, (swap i j).injective h)
           (λ b _, ⟨swap i j b, mem_univ _, by simp⟩),
-      by simp [sign_mul, this, sign_swap hij, prod_mul_distrib])
+      by simp [this, sign_swap hij, prod_mul_distrib])
     (λ σ _ _, (not_congr mul_swap_eq_iff).mpr hij)
     (λ _ _, mem_univ _)
     (λ σ _, mul_swap_involutive i j σ)
@@ -93,7 +93,7 @@ calc det (M ⬝ N) = ∑ p : n → n, ∑ σ : perm n, ε σ * ∏ i, (M (σ i)
         by rw ← σ⁻¹.prod_comp; simp [mul_apply],
       have h : ε σ * ε (τ * σ⁻¹) = ε τ :=
         calc ε σ * ε (τ * σ⁻¹) = ε ((τ * σ⁻¹) * σ) :
-          by rw [mul_comm, sign_mul (τ * σ⁻¹)]; simp [sign_mul]
+          by rw [mul_comm, sign_mul (τ * σ⁻¹)]; simp
         ... = ε τ : by simp,
       by rw h; simp [this, mul_comm, mul_assoc, mul_left_comm])
     (λ _ _ _ _, mul_right_cancel) (λ τ _, ⟨τ * σ, by simp⟩))