mark few more lemmas with ftrans_simp

lecopivo · Nov 28, 2023 · ff16552 · ff16552
1 parent 5d2b838
commit ff16552
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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