∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : DecidableEq l]
  [inst_1 : DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α) (e : m ≃ l) (f : n ≃ o),
  ((Matrix.reindex e f) A).updateRow i r = (Matrix.reindex e f) (A.updateRow (e.symm i) fun j => r (f j))