∀ {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 : m) (r : n → α) (e : l ≃ m) (f : o ≃ n),
  (A.updateRow i r).submatrix ⇑e ⇑f = (A.submatrix ⇑e ⇑f).updateRow (e.symm i) fun i => r (f i)