case a.h
l : Type ?u.1224395
m : Type u_2
n : Type u_1
o : Type ?u.1224404
m' : o → Type ?u.1224409
n' : o → Type ?u.1224414
R : Type ?u.1224417
S : Type ?u.1224420
α : Type v
β : Type w
γ : Type ?u.1224427
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
x✝ : n
⊢ map (updateColumn M j c) f i✝ x✝ = updateColumn (map M f) j (f ∘ c) i✝ x✝
l : Type ?u.1224395
m : Type u_2
n : Type u_1
o : Type ?u.1224404
m' : o → Type ?u.1224409
n' : o → Type ?u.1224414
R : Type ?u.1224417
S : Type ?u.1224420
α : Type v
β : Type w
γ : Type ?u.1224427
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
f : α → β
⊢ map (updateColumn M j c) f = updateColumn (map M f) j (f ∘ c)
ext
case a.h
l : Type ?u.1224395
m : Type u_2
n : Type u_1
o : Type ?u.1224404
m' : o → Type ?u.1224409
n' : o → Type ?u.1224414
R : Type ?u.1224417
S : Type ?u.1224420
α : Type v
β : Type w
γ : Type ?u.1224427
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
x✝ : n
⊢ f (if x✝ = j then c i✝ else M i✝ x✝) = if x✝ = j then (f ∘ c) i✝ else f (M i✝ x✝)
case a.h
l : Type ?u.1224395
m : Type u_2
n : Type u_1
o : Type ?u.1224404
m' : o → Type ?u.1224409
n' : o → Type ?u.1224414
R : Type ?u.1224417
S : Type ?u.1224420
α : Type v
β : Type w
γ : Type ?u.1224427
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
x✝ : n
⊢ map (updateColumn M j c) f i✝ x✝ = updateColumn (map M f) j (f ∘ c) i✝ x✝
rw [updateColumn_apply, map_apply, map_apply, updateColumn_apply]
no goals
case a.h
l : Type ?u.1224395
m : Type u_2
n : Type u_1
o : Type ?u.1224404
m' : o → Type ?u.1224409
n' : o → Type ?u.1224414
R : Type ?u.1224417
S : Type ?u.1224420
α : Type v
β : Type w
γ : Type ?u.1224427
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
x✝ : n
⊢ f (if x✝ = j then c i✝ else M i✝ x✝) = if x✝ = j then (f ∘ c) i✝ else f (M i✝ x✝)
exact apply_ite f _ _ _