diff --git a/tests/lean/run/matrix.lean b/tests/lean/run/matrix.lean
index a26ff9f3e..2cdcac4f7 100644
--- a/tests/lean/run/matrix.lean
+++ b/tests/lean/run/matrix.lean
@@ -5,8 +5,7 @@ variable same_dim {A : Type} : matrix A → matrix A → Prop
 variable add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A
 
 theorem same_dim_irrel {A : Type} {m1 m2 : matrix A} {H1 H2 : same_dim m1 m2} : @add A m1 m2 H1 = @add A m1 m2 H2 :=
-have eq : H1 = H2, from rfl,
-subst eq rfl
+rfl
 
 theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : same_dim m1' m2' :=
 subst H1 (subst H2 H)