Apply suggestions from code review

Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

Mathlib/LinearAlgebra/Matrix/Permanent.lean

@@ -93,34 +93,18 @@ theorem permanent_smul (M : Matrix n n R) (c : R) :
   exact prod_mul_pow_card.symm
 
 @[simp]
-theorem permanent_upodateRow_smul (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
+theorem permanent_updateRow_smul (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
     permanent (updateRow M j <| c • u) = c * permanent (updateRow M j u) := by
-  repeat rw [permanent]
-  rw [Finset.mul_sum]
-  congr
-  ext p
-  have h : p⁻¹ j ∈ univ := mem_univ _
-  repeat rw [← mul_prod_erase (Finset.univ ) _ h]
-  simp only [← mul_assoc, Perm.apply_inv_self, updateRow_self]
-  congr 1
-  apply Finset.prod_congr rfl
-  intro i hi
-  have : p i ≠ j := by aesop
-  simp [this]
+  rw [← permanent_transpose, ← updateColumn_transpose, permanent_updateColumn_smul,
+    updateColumn_transpose, permanent_transpose]
 
 @[simp]
-theorem permanent_upodateColumn_smul (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
+theorem permanent_updateColumn_smul (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
     permanent (updateColumn M j <| c • u) = c * permanent (updateColumn M j u) := by
-  repeat rw [permanent]
-  rw [Finset.mul_sum]
-  congr
-  ext p
-  have h : j ∈ univ := mem_univ _
-  repeat rw [← mul_prod_erase (Finset.univ ) _ h]
-  simp only [← mul_assoc, updateColumn_self]
-  congr 1
-  apply Finset.prod_congr rfl
-  intro i hi
-  simp [ne_of_mem_erase hi]
+  simp only [permanent, ← mul_prod_erase _ _ (mem_univ j), updateColumn_self, Pi.smul_apply,
+    smul_eq_mul, mul_sum, ← mul_assoc]
+  congr 1 with p
+  rw [Finset.prod_congr rfl (fun i hi ↦ ?_)]
+  simp only [ne_eq, ne_of_mem_erase hi, not_false_eq_true, updateColumn_ne]
 
 end Matrix