diff --git a/Mathlib/LinearAlgebra/Matrix/Block.lean b/Mathlib/LinearAlgebra/Matrix/Block.lean
index b723063aa7e338..acb3aa256054fa 100644
--- a/Mathlib/LinearAlgebra/Matrix/Block.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Block.lean
@@ -263,8 +263,7 @@ protected theorem BlockTriangular.det [DecidableEq α] [LinearOrder α] (hM : Bl
     let he : { a // b' a = l } ≃ { a // b a = l } :=
       haveI hc : ∀ i, b i = l → b i ≠ k := fun i hi => ne_of_eq_of_ne hi (ne_of_mem_erase hl)
       Equiv.subtypeSubtypeEquivSubtype @hc
-    simp only [toSquareBlock_def]
-    erw [← Matrix.det_reindex_self he.symm fun i j : { a // b a = l } => M ↑i ↑j]
+    rw [toSquareBlock_def, ← Matrix.det_reindex_self he.symm]
     rfl
   · intro i hi j hj
     apply hM