case a.h
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
⊢ updateColumn (diagonal v) i (Pi.single i x) j k = diagonal (Function.update v i x) j k
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
⊢ updateColumn (diagonal v) i (Pi.single i x) = diagonal (Function.update v i x)
ext j k
case a.h.inl
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ updateColumn (diagonal v) i (Pi.single i x) j j = diagonal (Function.update v i x) j j

case a.h.inr
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ updateColumn (diagonal v) i (Pi.single i x) j k = diagonal (Function.update v i x) j k
case a.h
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
⊢ updateColumn (diagonal v) i (Pi.single i x) j k = diagonal (Function.update v i x) j k
obtain rfl | hjk := eq_or_ne j k
case a.h.inl
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ updateColumn (diagonal v) i (Pi.single i x) j j = Function.update v i x j
case a.h.inl
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ updateColumn (diagonal v) i (Pi.single i x) j j = diagonal (Function.update v i x) j j
rw [diagonal_apply_eq]
case a.h.inl.inl
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j : n
⊢ updateColumn (diagonal v) j (Pi.single j x) j j = Function.update v j x j

case a.h.inl.inr
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ updateColumn (diagonal v) i (Pi.single i x) j j = Function.update v i x j
case a.h.inl
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ updateColumn (diagonal v) i (Pi.single i x) j j = Function.update v i x j
obtain rfl | hji := eq_or_ne j i
no goals
case a.h.inl.inl
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j : n
⊢ updateColumn (diagonal v) j (Pi.single j x) j j = Function.update v j x j
rw [updateColumn_self, Pi.single_eq_same, Function.update_same]
no goals
case a.h.inl.inr
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ updateColumn (diagonal v) i (Pi.single i x) j j = Function.update v i x j
rw [updateColumn_ne hji, diagonal_apply_eq, Function.update_noteq hji]
case a.h.inr
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ updateColumn (diagonal v) i (Pi.single i x) j k = 0
case a.h.inr
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ updateColumn (diagonal v) i (Pi.single i x) j k = diagonal (Function.update v i x) j k
rw [diagonal_apply_ne _ hjk]
case a.h.inr.inl
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ updateColumn (diagonal v) k (Pi.single k x) j k = 0

case a.h.inr.inr
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ updateColumn (diagonal v) i (Pi.single i x) j k = 0
case a.h.inr
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ updateColumn (diagonal v) i (Pi.single i x) j k = 0
obtain rfl | hki := eq_or_ne k i
no goals
case a.h.inr.inl
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ updateColumn (diagonal v) k (Pi.single k x) j k = 0
rw [updateColumn_self, Pi.single_eq_of_ne hjk]
no goals
case a.h.inr.inr
l : Type ?u.1229996
m : Type ?u.1229999
n : Type u_1
o : Type ?u.1230005
m' : o → Type ?u.1230010
n' : o → Type ?u.1230015
R : Type ?u.1230018
S : Type ?u.1230021
α : Type v
β : Type w
γ : Type ?u.1230028
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ updateColumn (diagonal v) i (Pi.single i x) j k = 0
rw [updateColumn_ne hki, diagonal_apply_ne _ hjk]