no goals
l : Type u_4
m : Type u_3
n : Type u_2
o : Type u_1
m' : o → Type ?u.1240817
n' : o → Type ?u.1240822
R : Type ?u.1240825
S : Type ?u.1240828
α : Type v
β : Type w
γ : Type ?u.1240835
M : Matrix m n α
i : m
j✝ : n
b : n → α
c✝ : m → α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq n
A : Matrix m n α
j : n
c : m → α
e : l ≃ m
f : o ≃ n
⊢ submatrix (updateColumn A j c) ↑e ↑f = submatrix (updateColumn A (↑f (↑f.symm j)) fun i => c (↑e (↑e.symm i))) ↑e ↑f
simp_rw [Equiv.apply_symm_apply]