refactor(data/matrix/basic): work around leanprover/lean4#2042 (#18696)

This adjust definitions such that everything is well-behaved in the case that things are unfolded. For each such definition, a lemma is added that replaces the equation lemma. Before this PR, we used
```lean
def transpose (M : matrix m n α) : matrix n m α
| x y := M y x
```
which has the nice behavior (in Lean 3 only) of `rw transpose` only unfolding the definition when it is of the applied form `transpose M i j`. If `dunfold transpose` is used then it becomes the undesirable `λ x y, M y x` in both Lean versions. After this PR, we use
```lean
def transpose (M : matrix m n α) : matrix n m α :=
of $ λ x y, M y x

-- TODO: set as an equation lemma for `transpose`, see mathlib4#3024
@[simp] lemma transpose_apply (M : matrix m n α) (i j) :
  transpose M i j = M j i := rfl
```
This no longer has the nice `rw` behavior, but we can't have that in Lean4 anyway (leanprover/lean4#2042). It also makes `dunfold` insert the `of`, which is better for type-safety.

This affects
* `matrix.transpose`
* `matrix.row`
* `matrix.col`
* `matrix.diagonal`
* `matrix.vec_mul_vec`
* `matrix.block_diagonal`
* `matrix.block_diagonal'`
* `matrix.hadamard`
* `matrix.kronecker_map`
* `pequiv.to_matrix`
* `matrix.circulant`
* `matrix.mv_polynomial_X`
* `algebra.trace_matrix`
* `algebra.embeddings_matrix`

While this just adds `_apply` noise in Lean 3, it is necessary when porting to Lean 4 as there the equation lemma is not generated in the way that we want.

This is hopefully exhaustive; it was found by looking for lines ending in `matrix .*` followed by a `|` line

Author: eric-wieser

src/algebra/lie/classical.lean

@@ -328,7 +328,7 @@ begin
   ext i j,
   rcases i with ⟨⟨i₁ | i₂⟩ | i₃⟩;
   rcases j with ⟨⟨j₁ | j₂⟩ | j₃⟩;
-  simp only [indefinite_diagonal, matrix.diagonal, equiv.sum_assoc_apply_inl_inl,
+  simp only [indefinite_diagonal, matrix.diagonal_apply, equiv.sum_assoc_apply_inl_inl,
     matrix.reindex_lie_equiv_apply, matrix.submatrix_apply, equiv.symm_symm, matrix.reindex_apply,
     sum.elim_inl, if_true, eq_self_iff_true, matrix.one_apply_eq, matrix.from_blocks_apply₁₁,
     dmatrix.zero_apply, equiv.sum_assoc_apply_inl_inr, if_false, matrix.from_blocks_apply₁₂,

src/combinatorics/simple_graph/adj_matrix.lean

@@ -148,11 +148,12 @@ variables (α)
 
 /-- `adj_matrix G α` is the matrix `A` such that `A i j = (1 : α)` if `i` and `j` are
   adjacent in the simple graph `G`, and otherwise `A i j = 0`. -/
-def adj_matrix [has_zero α] [has_one α] : matrix V V α
-| i j := if (G.adj i j) then 1 else 0
+def adj_matrix [has_zero α] [has_one α] : matrix V V α :=
+of $ λ i j, if (G.adj i j) then (1 : α) else 0
 
 variable {α}
 
+-- TODO: set as an equation lemma for `adj_matrix`, see mathlib4#3024
 @[simp]
 lemma adj_matrix_apply (v w : V) [has_zero α] [has_one α] :
   G.adj_matrix α v w = if (G.adj v w) then 1 else 0 := rfl

src/data/matrix/basic.lean

@@ -76,10 +76,14 @@ The two sides of the equivalence are definitionally equal types. We want to use
 to distinguish the types because `matrix` has different instances to pi types (such as `pi.has_mul`,
 which performs elementwise multiplication, vs `matrix.has_mul`).
 
-If you are defining a matrix, in terms of its entries, either use `of (λ i j, _)`, or use pattern
-matching in a definition as `| i j := _` (which can only be unfolded when fully-applied). The
-purpose of this approach is to ensure that terms of the form `(λ i j, _) * (λ i j, _)` do not
+If you are defining a matrix, in terms of its entries, use `of (λ i j, _)`. The
+purpose of this approach is to ensure that terms of th
+e form `(λ i j, _) * (λ i j, _)` do not
 appear, as the type of `*` can be misleading.
+
+Porting note: In Lean 3, it is also safe to use pattern matching in a definition as `| i j := _`,
+which can only be unfolded when fully-applied. leanprover/lean4#2042 means this does not
+(currently) work in Lean 4.
 -/
 def of : (m → n → α) ≃ matrix m n α := equiv.refl _
 @[simp] lemma of_apply (f : m → n → α) (i j) : of f i j = f i j := rfl
@@ -118,8 +122,12 @@ lemma map_injective {f : α → β} (hf : function.injective f) :
 λ M N h, ext $ λ i j, hf $ ext_iff.mpr h i j
 
 /-- The transpose of a matrix. -/
-def transpose (M : matrix m n α) : matrix n m α
-| x y := M y x
+def transpose (M : matrix m n α) : matrix n m α :=
+of $ λ x y, M y x
+
+-- TODO: set as an equation lemma for `transpose`, see mathlib4#3024
+@[simp] lemma transpose_apply (M : matrix m n α) (i j) :
+  transpose M i j = M j i := rfl
 
 localized "postfix (name := matrix.transpose) `ᵀ`:1500 := matrix.transpose" in matrix
 
@@ -130,12 +138,19 @@ M.transpose.map star
 localized "postfix (name := matrix.conj_transpose) `ᴴ`:1500 := matrix.conj_transpose" in matrix
 
 /-- `matrix.col u` is the column matrix whose entries are given by `u`. -/
-def col (w : m → α) : matrix m unit α
-| x y := w x
+def col (w : m → α) : matrix m unit α :=
+of $ λ x y, w x
+
+-- TODO: set as an equation lemma for `col`, see mathlib4#3024
+@[simp] lemma col_apply (w : m → α) (i j) :
+  col w i j = w i := rfl
 
 /-- `matrix.row u` is the row matrix whose entries are given by `u`. -/
-def row (v : n → α) : matrix unit n α
-| x y := v y
+def row (v : n → α) : matrix unit n α :=
+of $ λ x y, v y
+
+-- TODO: set as an equation lemma for `row`, see mathlib4#3024
+@[simp] lemma row_apply (v : n → α) (i j) : row v i j = v j := rfl
 
 instance [inhabited α] : inhabited (matrix m n α) := pi.inhabited _
 instance [has_add α] : has_add (matrix m n α) := pi.has_add
@@ -239,8 +254,12 @@ Note that bundled versions exist as:
 * `matrix.diagonal_ring_hom`
 * `matrix.diagonal_alg_hom`
 -/
-def diagonal [has_zero α] (d : n → α) : matrix n n α
-| i j := if i = j then d i else 0
+def diagonal [has_zero α] (d : n → α) : matrix n n α :=
+of $ λ i j, if i = j then d i else 0
+
+-- TODO: set as an equation lemma for `diagonal`, see mathlib4#3024
+lemma diagonal_apply [has_zero α] (d : n → α) (i j) : diagonal d i j = if i = j then d i else 0 :=
+rfl
 
 @[simp] theorem diagonal_apply_eq [has_zero α] (d : n → α) (i : n) : (diagonal d) i i = d i :=
 by simp [diagonal]
@@ -302,7 +321,7 @@ variables {n α R}
 
 @[simp] lemma diagonal_map [has_zero α] [has_zero β] {f : α → β} (h : f 0 = 0) {d : n → α} :
   (diagonal d).map f = diagonal (λ m, f (d m)) :=
-by { ext, simp only [diagonal, map_apply], split_ifs; simp [h], }
+by { ext, simp only [diagonal_apply, map_apply], split_ifs; simp [h], }
 
 @[simp] lemma diagonal_conj_transpose [add_monoid α] [star_add_monoid α] (v : n → α) :
   (diagonal v)ᴴ = diagonal (star v) :=
@@ -1113,8 +1132,13 @@ namespace matrix
 
 /-- For two vectors `w` and `v`, `vec_mul_vec w v i j` is defined to be `w i * v j`.
     Put another way, `vec_mul_vec w v` is exactly `col w ⬝ row v`. -/
-def vec_mul_vec [has_mul α] (w : m → α) (v : n → α) : matrix m n α
-| x y := w x * v y
+def vec_mul_vec [has_mul α] (w : m → α) (v : n → α) : matrix m n α :=
+of $ λ x y, w x * v y
+
+-- TODO: set as an equation lemma for `vec_mul_vec`, see mathlib4#3024
+lemma vec_mul_vec_apply [has_mul α] (w : m → α) (v : n → α) (i j) :
+  vec_mul_vec w v i j = w i * v j :=
+rfl
 
 lemma vec_mul_vec_eq [has_mul α] [add_comm_monoid α] (w : m → α) (v : n → α) :
   vec_mul_vec w v = (col w) ⬝ (row v) :=
@@ -1336,13 +1360,6 @@ section transpose
 
 open_locale matrix
 
-/--
-  Tell `simp` what the entries are in a transposed matrix.
-
-  Compare with `mul_apply`, `diagonal_apply_eq`, etc.
--/
-@[simp] lemma transpose_apply (M : matrix m n α) (i j) : M.transpose j i = M i j := rfl
-
 @[simp] lemma transpose_transpose (M : matrix m n α) :
   Mᵀᵀ = M :=
 by ext; refl
@@ -1353,7 +1370,7 @@ by ext i j; refl
 @[simp] lemma transpose_one [decidable_eq n] [has_zero α] [has_one α] : (1 : matrix n n α)ᵀ = 1 :=
 begin
   ext i j,
-  unfold has_one.one transpose,
+  rw [transpose_apply, ←diagonal_one],
   by_cases i = j,
   { simp only [h, diagonal_apply_eq] },
   { simp only [diagonal_apply_ne _ h, diagonal_apply_ne' _ h] }
@@ -1435,6 +1452,8 @@ def transpose_ring_equiv [add_comm_monoid α] [comm_semigroup α] [fintype m] :
   inv_fun := λ M, M.unopᵀ,
   map_mul' := λ M N, (congr_arg mul_opposite.op (transpose_mul M N)).trans
     (mul_opposite.op_mul _ _),
+  left_inv := λ M, transpose_transpose M,
+  right_inv := λ M, mul_opposite.unop_injective $ transpose_transpose M.unop,
   ..(transpose_add_equiv m m α).trans mul_opposite.op_add_equiv }
 
 variables {m α}
@@ -1895,9 +1914,6 @@ by { ext, refl }
 @[simp] lemma row_smul [has_smul R α] (x : R) (v : m → α) : row (x • v) = x • row v :=
 by { ext, refl }
 
-@[simp] lemma col_apply (v : m → α) (i j) : matrix.col v i j = v i := rfl
-@[simp] lemma row_apply (v : m → α) (i j) : matrix.row v i j = v j := rfl
-
 @[simp]
 lemma transpose_col (v : m → α) : (matrix.col v)ᵀ = matrix.row v := by { ext, refl }
 @[simp]

src/data/matrix/block.lean

@@ -278,8 +278,13 @@ the diagonal and zero elsewhere.
 
 See also `matrix.block_diagonal'` if the matrices may not have the same size everywhere.
 -/
-def block_diagonal (M : o → matrix m n α) : matrix (m × o) (n × o) α
-| ⟨i, k⟩ ⟨j, k'⟩ := if k = k' then M k i j else 0
+def block_diagonal (M : o → matrix m n α) : matrix (m × o) (n × o) α :=
+of $ (λ ⟨i, k⟩ ⟨j, k'⟩, if k = k' then M k i j else 0 : m × o → n × o → α)
+
+-- TODO: set as an equation lemma for `block_diagonal`, see mathlib4#3024
+lemma block_diagonal_apply' (M : o → matrix m n α) (i k j k') :
+  block_diagonal M ⟨i, k⟩ ⟨j, k'⟩ = if k = k' then M k i j else 0 :=
+rfl
 
 lemma block_diagonal_apply (M : o → matrix m n α) (ik jk) :
   block_diagonal M ik jk = if ik.2 = jk.2 then M ik.2 ik.1 jk.1 else 0 :=
@@ -328,7 +333,7 @@ by { ext, simp [block_diagonal_apply] }
   block_diagonal (λ k, diagonal (d k)) = diagonal (λ ik, d ik.2 ik.1) :=
 begin
   ext ⟨i, k⟩ ⟨j, k'⟩,
-  simp only [block_diagonal_apply, diagonal, prod.mk.inj_iff, ← ite_and],
+  simp only [block_diagonal_apply, diagonal_apply, prod.mk.inj_iff, ← ite_and],
   congr' 1,
   rw and_comm,
 end
@@ -404,8 +409,12 @@ section block_diag
 /-- Extract a block from the diagonal of a block diagonal matrix.
 
 This is the block form of `matrix.diag`, and the left-inverse of `matrix.block_diagonal`. -/
-def block_diag (M : matrix (m × o) (n × o) α) (k : o) : matrix m n α
-| i j := M (i, k) (j, k)
+def block_diag (M : matrix (m × o) (n × o) α) (k : o) : matrix m n α :=
+of $ λ i j, M (i, k) (j, k)
+
+-- TODO: set as an equation lemma for `block_diag`, see mathlib4#3024
+lemma block_diag_apply (M : matrix (m × o) (n × o) α) (k : o) (i j) :
+  block_diag M k i j = M (i, k) (j, k) := rfl
 
 lemma block_diag_map (M : matrix (m × o) (n × o) α) (f : α → β) :
   block_diag (M.map f) = λ k, (block_diag M k).map f :=
@@ -431,14 +440,14 @@ rfl
   block_diag (diagonal d) k = diagonal (λ i, d (i, k)) :=
 ext $ λ i j, begin
   obtain rfl | hij := decidable.eq_or_ne i j,
-  { rw [block_diag, diagonal_apply_eq, diagonal_apply_eq] },
-  { rw [block_diag, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt _ hij)],
+  { rw [block_diag_apply, diagonal_apply_eq, diagonal_apply_eq] },
+  { rw [block_diag_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt _ hij)],
     exact prod.fst_eq_iff.mpr },
 end
 
 @[simp] lemma block_diag_block_diagonal [decidable_eq o] (M : o → matrix m n α) :
   block_diag (block_diagonal M) = M :=
-funext $ λ k, ext $ λ i j, block_diagonal_apply_eq _ _ _ _
+funext $ λ k, ext $ λ i j, block_diagonal_apply_eq M i j _
 
 @[simp] lemma block_diag_one [decidable_eq o] [decidable_eq m] [has_one α] :
   block_diag (1 : matrix (m × o) (m × o) α) = 1 :=
@@ -486,8 +495,15 @@ variables [has_zero α] [has_zero β]
 and zero elsewhere.
 
 This is the dependently-typed version of `matrix.block_diagonal`. -/
-def block_diagonal' (M : Π i, matrix (m' i) (n' i) α) : matrix (Σ i, m' i) (Σ i, n' i) α
-| ⟨k, i⟩ ⟨k', j⟩ := if h : k = k' then M k i (cast (congr_arg n' h.symm) j) else 0
+def block_diagonal' (M : Π i, matrix (m' i) (n' i) α) : matrix (Σ i, m' i) (Σ i, n' i) α :=
+of $ (λ ⟨k, i⟩ ⟨k', j⟩, if h : k = k' then M k i (cast (congr_arg n' h.symm) j) else 0 :
+  (Σ i, m' i) → (Σ i, n' i) → α)
+
+-- TODO: set as an equation lemma for `block_diagonal'`, see mathlib4#3024
+lemma block_diagonal'_apply' (M : Π i, matrix (m' i) (n' i) α) (k i k' j) :
+  block_diagonal' M ⟨k, i⟩ ⟨k', j⟩ =
+    if h : k = k' then M k i (cast (congr_arg n' h.symm) j) else 0 :=
+rfl
 
 lemma block_diagonal'_eq_block_diagonal (M : o → matrix m n α) {k k'} (i j) :
   block_diagonal M (i, k) (j, k') = block_diagonal' M ⟨k, i⟩ ⟨k', j⟩ :=
@@ -625,8 +641,12 @@ section block_diag'
 /-- Extract a block from the diagonal of a block diagonal matrix.
 
 This is the block form of `matrix.diag`, and the left-inverse of `matrix.block_diagonal'`. -/
-def block_diag' (M : matrix (Σ i, m' i) (Σ i, n' i) α) (k : o) : matrix (m' k) (n' k) α
-| i j := M ⟨k, i⟩ ⟨k, j⟩
+def block_diag' (M : matrix (Σ i, m' i) (Σ i, n' i) α) (k : o) : matrix (m' k) (n' k) α :=
+of $ λ i j, M ⟨k, i⟩ ⟨k, j⟩
+
+-- TODO: set as an equation lemma for `block_diag'`, see mathlib4#3024
+lemma block_diag'_apply (M : matrix (Σ i, m' i) (Σ i, n' i) α) (k : o) (i j) :
+  block_diag' M k i j = M ⟨k, i⟩ ⟨k, j⟩ := rfl
 
 lemma block_diag'_map (M : matrix (Σ i, m' i) (Σ i, n' i) α) (f : α → β) :
   block_diag' (M.map f) = λ k, (block_diag' M k).map f :=
@@ -653,14 +673,14 @@ rfl
   block_diag' (diagonal d) k = diagonal (λ i, d ⟨k, i⟩) :=
 ext $ λ i j, begin
   obtain rfl | hij := decidable.eq_or_ne i j,
-  { rw [block_diag', diagonal_apply_eq, diagonal_apply_eq] },
-  { rw [block_diag', diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt (λ h, _) hij)],
+  { rw [block_diag'_apply, diagonal_apply_eq, diagonal_apply_eq] },
+  { rw [block_diag'_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt (λ h, _) hij)],
     cases h, refl },
 end
 
 @[simp] lemma block_diag'_block_diagonal' [decidable_eq o] (M : Π i, matrix (m' i) (n' i) α) :
   block_diag' (block_diagonal' M) = M :=
-funext $ λ k, ext $ λ i j, block_diagonal'_apply_eq _ _ _ _
+funext $ λ k, ext $ λ i j, block_diagonal'_apply_eq M _ _ _
 
 @[simp] lemma block_diag'_one [decidable_eq o] [Π i, decidable_eq (m' i)] [has_one α] :
   block_diag' (1 : matrix (Σ i, m' i) (Σ i, m' i) α) = 1 :=

src/data/matrix/hadamard.lean

@@ -37,10 +37,13 @@ open_locale matrix big_operators
 
 /-- `matrix.hadamard` defines the Hadamard product,
     which is the pointwise product of two matrices of the same size.-/
-@[simp]
-def hadamard [has_mul α] (A : matrix m n α) (B : matrix m n α) : matrix m n α
-| i j := A i j * B i j
+def hadamard [has_mul α] (A : matrix m n α) (B : matrix m n α) : matrix m n α :=
+of $ λ i j, A i j * B i j
 
+-- TODO: set as an equation lemma for `hadamard`, see mathlib4#3024
+@[simp]
+lemma hadamard_apply [has_mul α] (A : matrix m n α) (B : matrix m n α) (i j) :
+  hadamard A B i j = A i j * B i j := rfl
 localized "infix (name := matrix.hadamard) ` ⊙ `:100 := matrix.hadamard" in matrix
 
 section basic_properties

src/data/matrix/kronecker.lean

@@ -52,9 +52,14 @@ variables {l m n p : Type*} {q r : Type*} {l' m' n' p' : Type*}
 section kronecker_map
 
 /-- Produce a matrix with `f` applied to every pair of elements from `A` and `B`. -/
-@[simp] def kronecker_map (f : α → β → γ) (A : matrix l m α) (B : matrix n p β) :
-  matrix (l × n) (m × p) γ
-| i j := f (A i.1 j.1) (B i.2 j.2)
+def kronecker_map (f : α → β → γ) (A : matrix l m α) (B : matrix n p β) :
+  matrix (l × n) (m × p) γ :=
+of $ λ (i : l × n) (j : m × p), f (A i.1 j.1) (B i.2 j.2)
+
+-- TODO: set as an equation lemma for `kronecker_map`, see mathlib4#3024
+@[simp]
+lemma kronecker_map_apply (f : α → β → γ) (A : matrix l m α) (B : matrix n p β) (i j) :
+  kronecker_map f A B i j = f (A i.1 j.1) (B i.2 j.2) := rfl
 
 lemma kronecker_map_transpose (f : α → β → γ)
   (A : matrix l m α) (B : matrix n p β) :
@@ -199,7 +204,7 @@ lemma kronecker_map_bilinear_mul_mul [comm_semiring R]
 begin
   ext ⟨i, i'⟩ ⟨j, j'⟩,
   simp only [kronecker_map_bilinear_apply_apply, mul_apply, ← finset.univ_product_univ,
-    finset.sum_product, kronecker_map],
+    finset.sum_product, kronecker_map_apply],
   simp_rw [f.map_sum, linear_map.sum_apply, linear_map.map_sum, h_comm],
 end
 
@@ -212,7 +217,7 @@ lemma trace_kronecker_map_bilinear [comm_semiring R]
   (f : α →ₗ[R] β →ₗ[R] γ) (A : matrix m m α) (B : matrix n n β) :
   trace (kronecker_map_bilinear f A B) = f (trace A) (trace B) :=
 by simp_rw [matrix.trace, matrix.diag, kronecker_map_bilinear_apply_apply,
-  linear_map.map_sum₂, map_sum, ←finset.univ_product_univ, finset.sum_product, kronecker_map]
+  linear_map.map_sum₂, map_sum, ←finset.univ_product_univ, finset.sum_product, kronecker_map_apply]
 
 /-- `determinant` of `matrix.kronecker_map_bilinear`.
 

src/data/matrix/notation.lean

@@ -285,7 +285,7 @@ by { ext i, refine fin.cases _ _ i; simp [vec_mul_vec] }
 
 @[simp] lemma vec_mul_vec_cons (v : m' → α) (x : α) (w : fin n → α) :
   vec_mul_vec v (vec_cons x w) = λ i, v i • vec_cons x w :=
-by { ext i j, rw [vec_mul_vec, pi.smul_apply, smul_eq_mul] }
+by { ext i j, rw [vec_mul_vec_apply, pi.smul_apply, smul_eq_mul] }
 
 end vec_mul_vec
 

src/data/matrix/pequiv.lean

@@ -44,8 +44,13 @@ open_locale matrix
 
 /-- `to_matrix` returns a matrix containing ones and zeros. `f.to_matrix i j` is `1` if
   `f i = some j` and `0` otherwise -/
-def to_matrix [decidable_eq n] [has_zero α] [has_one α] (f : m ≃. n) : matrix m n α
-| i j := if j ∈ f i then 1 else 0
+def to_matrix [decidable_eq n] [has_zero α] [has_one α] (f : m ≃. n) : matrix m n α :=
+of $ λ i j, if j ∈ f i then (1 : α) else 0
+
+-- TODO: set as an equation lemma for `to_matrix`, see mathlib4#3024
+@[simp]
+lemma to_matrix_apply [decidable_eq n] [has_zero α] [has_one α] (f : m ≃. n) (i j) :
+  to_matrix f i j = if j ∈ f i then (1 : α) else 0 := rfl
 
 lemma mul_matrix_apply [fintype m] [decidable_eq m] [semiring α] (f : l ≃. m) (M : matrix m n α)
   (i j) : (f.to_matrix ⬝ M) i j = option.cases_on (f i) 0 (λ fi, M fi j) :=
@@ -59,11 +64,11 @@ end
 
 lemma to_matrix_symm [decidable_eq m] [decidable_eq n] [has_zero α] [has_one α] (f : m ≃. n) :
   (f.symm.to_matrix : matrix n m α) = f.to_matrixᵀ :=
-by ext; simp only [transpose, mem_iff_mem f, to_matrix]; congr
+by ext; simp only [transpose, mem_iff_mem f, to_matrix_apply]; congr
 
 @[simp] lemma to_matrix_refl [decidable_eq n] [has_zero α] [has_one α] :
   ((pequiv.refl n).to_matrix : matrix n n α) = 1 :=
-by ext; simp [to_matrix, one_apply]; congr
+by ext; simp [to_matrix_apply, one_apply]; congr
 
 lemma matrix_mul_apply [fintype m] [semiring α] [decidable_eq n] (M : matrix l m α) (f : m ≃. n)
   (i j) : (M ⬝ f.to_matrix) i j = option.cases_on (f.symm j) 0 (λ fj, M i fj) :=
@@ -104,7 +109,7 @@ begin
   classical,
   assume f g,
   refine not_imp_not.1 _,
-  simp only [matrix.ext_iff.symm, to_matrix, pequiv.ext_iff,
+  simp only [matrix.ext_iff.symm, to_matrix_apply, pequiv.ext_iff,
     not_forall, exists_imp_distrib],
   assume i hi,
   use i,