case a.h
l : Type ?u.197342
m : Type ?u.197345
n : Type ?u.197348
o : Type u_5
p : Type ?u.197354
q : Type ?u.197357
m' : o → Type u_1
n' : o → Type u_2
p' : o → Type ?u.197372
R : Type ?u.197375
S : Type ?u.197378
α : Type u_3
β : Type u_4
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ map (blockDiagonal' M) f i✝ x✝ = blockDiagonal' (fun k => map (M k) f) i✝ x✝
l : Type ?u.197342
m : Type ?u.197345
n : Type ?u.197348
o : Type u_5
p : Type ?u.197354
q : Type ?u.197357
m' : o → Type u_1
n' : o → Type u_2
p' : o → Type ?u.197372
R : Type ?u.197375
S : Type ?u.197378
α : Type u_3
β : Type u_4
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
⊢ map (blockDiagonal' M) f = blockDiagonal' fun k => map (M k) f
ext
case a.h
l : Type ?u.197342
m : Type ?u.197345
n : Type ?u.197348
o : Type u_5
p : Type ?u.197354
q : Type ?u.197357
m' : o → Type u_1
n' : o → Type u_2
p' : o → Type ?u.197372
R : Type ?u.197375
S : Type ?u.197378
α : Type u_3
β : Type u_4
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ f (if h : i✝.fst = x✝.fst then M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0) =
    if h : i✝.fst = x✝.fst then f (M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd)) else 0
case a.h
l : Type ?u.197342
m : Type ?u.197345
n : Type ?u.197348
o : Type u_5
p : Type ?u.197354
q : Type ?u.197357
m' : o → Type u_1
n' : o → Type u_2
p' : o → Type ?u.197372
R : Type ?u.197375
S : Type ?u.197378
α : Type u_3
β : Type u_4
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ 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.197342
m : Type ?u.197345
n : Type ?u.197348
o : Type u_5
p : Type ?u.197354
q : Type ?u.197357
m' : o → Type u_1
n' : o → Type u_2
p' : o → Type ?u.197372
R : Type ?u.197375
S : Type ?u.197378
α : Type u_3
β : Type u_4
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ f (if h : i✝.fst = x✝.fst then M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0) =
    if h : i✝.fst = x✝.fst then f (M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd)) else 0
rw [apply_dite f, hf]