feat(data/matrix/basic): add bit0, bit1 lemmas (#2987)

Based on a conversation in
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Matrix.20equality.20by.20extensionality
we define simp lemmas for matrices represented by numerals.
This should result in better representation of scalar multiples of
 `one_val : matrix n n a`.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/data/matrix/basic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2018 Ellen Arlt. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Ellen Arlt, Blair Shi, Sean Leather, Mario Carneiro, Johan Commelin
+Authors: Ellen Arlt, Blair Shi, Sean Leather, Mario Carneiro, Johan Commelin, Scott Morrison, Yakov Pechersky
 -/
 import algebra.pi_instances
 /-!
@@ -102,6 +102,13 @@ diagonal_val_ne'
 end one
 end diagonal
 
+@[simp] lemma bit0_apply_apply [has_add α] (M : matrix n n α) (i : n) (j : n) :
+  (bit0 M) i j = bit0 (M i j) := rfl
+
+@[simp] lemma bit1_apply_apply [decidable_eq n] [semiring α] (M : matrix n n α) (i : n) (j : n) :
+  (bit1 M) i j = if i = j then bit1 (M i j) else bit0 (M i j) :=
+by dsimp [bit1]; by_cases i = j; simp [h]
+
 @[simp] theorem diagonal_add [decidable_eq n] [add_monoid α] (d₁ d₂ : n → α) :
   diagonal d₁ + diagonal d₂ = diagonal (λ i, d₁ i + d₂ i) :=
 by ext i j; by_cases i = j; simp [h]