case pos
l : Type ?u.1220689
m : Type u_2
n : Type u_1
o : Type ?u.1220698
m' : o → Type ?u.1220703
n' : o → Type ?u.1220708
R : Type ?u.1220711
S : Type ?u.1220714
α : Type v
β : Type w
γ : Type ?u.1220721
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
j' : n
h : j' = j
⊢ updateColumn M j c i j' = if j' = j then c i else M i j'

case neg
l : Type ?u.1220689
m : Type u_2
n : Type u_1
o : Type ?u.1220698
m' : o → Type ?u.1220703
n' : o → Type ?u.1220708
R : Type ?u.1220711
S : Type ?u.1220714
α : Type v
β : Type w
γ : Type ?u.1220721
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ updateColumn M j c i j' = if j' = j then c i else M i j'
l : Type ?u.1220689
m : Type u_2
n : Type u_1
o : Type ?u.1220698
m' : o → Type ?u.1220703
n' : o → Type ?u.1220708
R : Type ?u.1220711
S : Type ?u.1220714
α : Type v
β : Type w
γ : Type ?u.1220721
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
j' : n
⊢ updateColumn M j c i j' = if j' = j then c i else M i j'
by_cases j' = j
no goals
case pos
l : Type ?u.1220689
m : Type u_2
n : Type u_1
o : Type ?u.1220698
m' : o → Type ?u.1220703
n' : o → Type ?u.1220708
R : Type ?u.1220711
S : Type ?u.1220714
α : Type v
β : Type w
γ : Type ?u.1220721
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
j' : n
h : j' = j
⊢ updateColumn M j c i j' = if j' = j then c i else M i j'
rw [h, updateColumn_self, if_pos rfl]
no goals
case neg
l : Type ?u.1220689
m : Type u_2
n : Type u_1
o : Type ?u.1220698
m' : o → Type ?u.1220703
n' : o → Type ?u.1220708
R : Type ?u.1220711
S : Type ?u.1220714
α : Type v
β : Type w
γ : Type ?u.1220721
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ updateColumn M j c i j' = if j' = j then c i else M i j'
rw [updateColumn_ne h, if_neg h]