not_true_eq_false now appears in test/matrix.lean's output

leanprover-community · Oct 22, 2023 · 828242f · 828242f
1 parent f68aedd
commit 828242f
Showing 1 changed file with 8 additions and 7 deletions.
diff --git a/test/matrix.lean b/test/matrix.lean
@@ -139,9 +139,10 @@ example {α : Type _} [CommRing α] {a b c d : α} :
     Matrix.det !![a, b; c, d] = a * d - b * c := by
   simp? [Matrix.det_succ_row_zero, Fin.sum_univ_succ] says
     simp only [det_succ_row_zero, Nat.odd_iff_not_even, of_apply, cons_val', empty_val',
-      cons_val_fin_one, cons_val_zero, det_unique, Fin.default_eq_zero, submatrix_apply, Fin.succ_zero_eq_one, ne_eq,
-      cons_val_one, head_fin_const, Fin.sum_univ_succ, Fin.val_zero, pow_zero, one_mul, Fin.zero_succAbove, head_cons,
-      Finset.univ_unique, Fin.val_succ, Fin.coe_fin_one, zero_add, pow_one, cons_val_succ, neg_mul,
+      cons_val_fin_one, cons_val_zero, det_unique, Fin.default_eq_zero, submatrix_apply,
+      Fin.succ_zero_eq_one, ne_eq, cons_val_one, head_fin_const, Fin.sum_univ_succ, Fin.val_zero,
+      pow_zero, one_mul, not_true_eq_false, Fin.zero_succAbove, head_cons, Finset.univ_unique,
+      Fin.val_succ, Fin.coe_fin_one, zero_add, pow_one, cons_val_succ, neg_mul,
       Fin.succ_succAbove_zero, Finset.sum_const, Finset.card_singleton, smul_neg, one_smul]
   ring
 
@@ -150,10 +151,10 @@ example {α : Type _} [CommRing α] {a b c d e f g h i : α} :
       a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g := by
   simp? [Matrix.det_succ_row_zero, Fin.sum_univ_succ] says
     simp only [det_succ_row_zero, Nat.odd_iff_not_even, of_apply, cons_val', empty_val',
-      cons_val_fin_one, cons_val_zero, submatrix_apply, Fin.succ_zero_eq_one, cons_val_one,
-      head_cons, submatrix_submatrix, det_unique, Fin.default_eq_zero, Function.comp_apply,
-      Fin.succ_one_eq_two, ne_eq, cons_val_two, tail_cons, head_fin_const, Fin.sum_univ_succ,
-      Fin.val_zero, pow_zero, one_mul, Fin.zero_succAbove, Finset.univ_unique, Fin.val_succ,
+      cons_val_fin_one, cons_val_zero, submatrix_apply, Fin.succ_zero_eq_one, cons_val_one, head_cons,
+      submatrix_submatrix, det_unique, Fin.default_eq_zero, Function.comp_apply, Fin.succ_one_eq_two,
+      ne_eq, cons_val_two, tail_cons, head_fin_const, Fin.sum_univ_succ, Fin.val_zero, pow_zero,
+      one_mul, not_true_eq_false, Fin.zero_succAbove, Finset.univ_unique, Fin.val_succ,
       Fin.coe_fin_one, zero_add, pow_one, neg_mul, Fin.succ_succAbove_zero, Finset.sum_neg_distrib,
       Finset.sum_singleton, cons_val_succ, Fin.succ_succAbove_one, even_add_self, Even.neg_pow,
       one_pow, Finset.sum_const, Finset.card_singleton, one_smul]