no goals
l : Type u_4
m : Type u_3
n : Type u_2
o : Type u_1
m' : o → Type ?u.1238605
n' : o → Type ?u.1238610
R : Type ?u.1238613
S : Type ?u.1238616
α : Type v
β : Type w
γ : Type ?u.1238623
M : Matrix m n α
i : m
j✝ : n
b : n → α
c✝ : m → α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq n
A : Matrix m n α
j : o
c : l → α
e : l ≃ m
f : o ≃ n
⊢ updateColumn (submatrix A ↑e ↑f) j c = submatrix (updateColumn A (↑f j) fun i => c (↑e.symm i)) ↑e ↑f
simpa only [← transpose_submatrix, updateRow_transpose] using
  congr_arg transpose (updateRow_submatrix_equiv Aᵀ j c f e)