case pos
l : Type ?u.1220174
m : Type u_1
n : Type u_2
o : Type ?u.1220183
m' : o → Type ?u.1220188
n' : o → Type ?u.1220193
R : Type ?u.1220196
S : Type ?u.1220199
α : Type v
β : Type w
γ : Type ?u.1220206
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i' : m
h : i' = i
⊢ updateRow M i b i' j = if i' = i then b j else M i' j

case neg
l : Type ?u.1220174
m : Type u_1
n : Type u_2
o : Type ?u.1220183
m' : o → Type ?u.1220188
n' : o → Type ?u.1220193
R : Type ?u.1220196
S : Type ?u.1220199
α : Type v
β : Type w
γ : Type ?u.1220206
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ updateRow M i b i' j = if i' = i then b j else M i' j
l : Type ?u.1220174
m : Type u_1
n : Type u_2
o : Type ?u.1220183
m' : o → Type ?u.1220188
n' : o → Type ?u.1220193
R : Type ?u.1220196
S : Type ?u.1220199
α : Type v
β : Type w
γ : Type ?u.1220206
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i' : m
⊢ updateRow M i b i' j = if i' = i then b j else M i' j
by_cases i' = i
no goals
case pos
l : Type ?u.1220174
m : Type u_1
n : Type u_2
o : Type ?u.1220183
m' : o → Type ?u.1220188
n' : o → Type ?u.1220193
R : Type ?u.1220196
S : Type ?u.1220199
α : Type v
β : Type w
γ : Type ?u.1220206
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i' : m
h : i' = i
⊢ updateRow M i b i' j = if i' = i then b j else M i' j
rw [h, updateRow_self, if_pos rfl]
no goals
case neg
l : Type ?u.1220174
m : Type u_1
n : Type u_2
o : Type ?u.1220183
m' : o → Type ?u.1220188
n' : o → Type ?u.1220193
R : Type ?u.1220196
S : Type ?u.1220199
α : Type v
β : Type w
γ : Type ?u.1220206
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ updateRow M i b i' j = if i' = i then b j else M i' j
rw [updateRow_ne h, if_neg h]