From ff16552383614ab4a35f66cb304db35a9e11c9d5 Mon Sep 17 00:00:00 2001 From: lecopivo Date: Tue, 28 Nov 2023 14:24:18 -0500 Subject: [PATCH] mark few more lemmas with ftrans_simp --- SciLean/Tactic/FTrans/Simp.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SciLean/Tactic/FTrans/Simp.lean b/SciLean/Tactic/FTrans/Simp.lean index 244450a1..60ed1800 100644 --- a/SciLean/Tactic/FTrans/Simp.lean +++ b/SciLean/Tactic/FTrans/Simp.lean @@ -5,6 +5,6 @@ import Mathlib.Algebra.SMulWithZero namespace SciLean -attribute [ftrans_simp] Prod.mk_add_mk Prod.mk_mul_mk Prod.smul_mk Prod.mk_sub_mk Prod.neg_mk Prod.vadd_mk add_zero zero_add sub_zero zero_sub sub_self neg_zero mul_zero zero_mul zero_smul smul_zero smul_eq_mul smul_neg eq_self iff_self mul_one one_mul one_smul +attribute [ftrans_simp] Prod.mk_add_mk Prod.mk_mul_mk Prod.smul_mk Prod.mk_sub_mk Prod.neg_mk Prod.vadd_mk add_zero zero_add sub_zero zero_sub sub_self neg_zero mul_zero zero_mul zero_smul smul_zero smul_eq_mul smul_neg eq_self iff_self mul_one one_mul one_smul Prod.fst_zero Prod.snd_zero attribute [ftrans_simp] Equiv.invFun_as_coe Equiv.symm_symm