case a.h
l : Type ?u.129660
m : Type u_1
n : Type u_2
o : Type u_5
p : Type ?u.129672
q : Type ?u.129675
m' : o → Type ?u.129680
n' : o → Type ?u.129685
p' : o → Type ?u.129690
R : Type ?u.129693
S : Type ?u.129696
α : Type u_3
β : Type u_4
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
x✝ : n × o
⊢ map (blockDiagonal M) f i✝ x✝ = blockDiagonal (fun k => map (M k) f) i✝ x✝
l : Type ?u.129660
m : Type u_1
n : Type u_2
o : Type u_5
p : Type ?u.129672
q : Type ?u.129675
m' : o → Type ?u.129680
n' : o → Type ?u.129685
p' : o → Type ?u.129690
R : Type ?u.129693
S : Type ?u.129696
α : Type u_3
β : Type u_4
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
⊢ map (blockDiagonal M) f = blockDiagonal fun k => map (M k) f
ext
case a.h
l : Type ?u.129660
m : Type u_1
n : Type u_2
o : Type u_5
p : Type ?u.129672
q : Type ?u.129675
m' : o → Type ?u.129680
n' : o → Type ?u.129685
p' : o → Type ?u.129690
R : Type ?u.129693
S : Type ?u.129696
α : Type u_3
β : Type u_4
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
x✝ : n × o
⊢ f (if i✝.snd = x✝.snd then M i✝.snd i✝.fst x✝.fst else 0) = if i✝.snd = x✝.snd then f (M i✝.snd i✝.fst x✝.fst) else 0
case a.h
l : Type ?u.129660
m : Type u_1
n : Type u_2
o : Type u_5
p : Type ?u.129672
q : Type ?u.129675
m' : o → Type ?u.129680
n' : o → Type ?u.129685
p' : o → Type ?u.129690
R : Type ?u.129693
S : Type ?u.129696
α : Type u_3
β : Type u_4
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
x✝ : n × o
⊢ map (blockDiagonal M) f i✝ x✝ = blockDiagonal (fun k => map (M k) f) i✝ x✝
simp only [map_apply, blockDiagonal_apply, eq_comm]
no goals
case a.h
l : Type ?u.129660
m : Type u_1
n : Type u_2
o : Type u_5
p : Type ?u.129672
q : Type ?u.129675
m' : o → Type ?u.129680
n' : o → Type ?u.129685
p' : o → Type ?u.129690
R : Type ?u.129693
S : Type ?u.129696
α : Type u_3
β : Type u_4
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
x✝ : n × o
⊢ f (if i✝.snd = x✝.snd then M i✝.snd i✝.fst x✝.fst else 0) = if i✝.snd = x✝.snd then f (M i✝.snd i✝.fst x✝.fst) else 0
rw [apply_ite f, hf]