perf(Matrix.SpecialLinearGroup): clean up with dsimp first (#10738)

This reduces the number of instructions by over a third using `dsimp` to clean up an expression before starting a proof.
leanprover-community · Feb 20, 2024 · c9eb34f · c9eb34f
1 parent c39e9ef
commit c9eb34f
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
@@ -311,6 +311,7 @@ def center_equiv_rootsOfUnity' (i : n) :
     obtain ⟨⟨a, _⟩, ha⟩ := a
     refine SetCoe.ext <| Units.eq_iff.mp <| by simp
   map_mul' A B := by
+    dsimp
     ext
     simp only [Submonoid.coe_mul, coe_mul, rootsOfUnity.val_mkOfPowEq_coe, Units.val_mul]
     rw [← scalar_eq_coe_self_center A i, ← scalar_eq_coe_self_center B i]