case a.h
l : Type ?u.1223184
m : Type u_1
n : Type u_2
o : Type ?u.1223193
m' : o → Type ?u.1223198
n' : o → Type ?u.1223203
R : Type ?u.1223206
S : Type ?u.1223209
α : Type v
β : Type w
γ : Type ?u.1223216
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
x✝ : n
⊢ map (updateRow M i b) f i✝ x✝ = updateRow (map M f) i (f ∘ b) i✝ x✝
l : Type ?u.1223184
m : Type u_1
n : Type u_2
o : Type ?u.1223193
m' : o → Type ?u.1223198
n' : o → Type ?u.1223203
R : Type ?u.1223206
S : Type ?u.1223209
α : Type v
β : Type w
γ : Type ?u.1223216
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
f : α → β
⊢ map (updateRow M i b) f = updateRow (map M f) i (f ∘ b)
ext
case a.h
l : Type ?u.1223184
m : Type u_1
n : Type u_2
o : Type ?u.1223193
m' : o → Type ?u.1223198
n' : o → Type ?u.1223203
R : Type ?u.1223206
S : Type ?u.1223209
α : Type v
β : Type w
γ : Type ?u.1223216
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
x✝ : n
⊢ f (if i✝ = i then b x✝ else M i✝ x✝) = if i✝ = i then (f ∘ b) x✝ else f (M i✝ x✝)
case a.h
l : Type ?u.1223184
m : Type u_1
n : Type u_2
o : Type ?u.1223193
m' : o → Type ?u.1223198
n' : o → Type ?u.1223203
R : Type ?u.1223206
S : Type ?u.1223209
α : Type v
β : Type w
γ : Type ?u.1223216
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
x✝ : n
⊢ map (updateRow M i b) f i✝ x✝ = updateRow (map M f) i (f ∘ b) i✝ x✝
rw [updateRow_apply, map_apply, map_apply, updateRow_apply]
no goals
case a.h
l : Type ?u.1223184
m : Type u_1
n : Type u_2
o : Type ?u.1223193
m' : o → Type ?u.1223198
n' : o → Type ?u.1223203
R : Type ?u.1223206
S : Type ?u.1223209
α : Type v
β : Type w
γ : Type ?u.1223216
M : Matrix m n α
i : m
j : n
b : n → α
c : m → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
x✝ : n
⊢ f (if i✝ = i then b x✝ else M i✝ x✝) = if i✝ = i then (f ∘ b) x✝ else f (M i✝ x✝)
exact apply_ite f _ _ _