From 42a8fb5965b7ee83ddb183f2acfae6add05f65f3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Aug 2014 09:27:19 -0700 Subject: [PATCH] chore(tests/lean/run/matrix): simplify same_dim_irrel proof Signed-off-by: Leonardo de Moura --- tests/lean/run/matrix.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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)