case a.h
l : Type ?u.135132
m : Type u_1
n : Type u_2
o : Type u_3
p : Type ?u.135144
q : Type ?u.135147
m' : o → Type ?u.135152
n' : o → Type ?u.135157
p' : o → Type ?u.135162
R : Type ?u.135165
S : Type ?u.135168
α : Type u_4
β : Type ?u.135174
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
i✝ : m × o
x✝ : n × o
⊢ blockDiagonal 0 i✝ x✝ = OfNat.ofNat 0 i✝ x✝
l : Type ?u.135132
m : Type u_1
n : Type u_2
o : Type u_3
p : Type ?u.135144
q : Type ?u.135147
m' : o → Type ?u.135152
n' : o → Type ?u.135157
p' : o → Type ?u.135162
R : Type ?u.135165
S : Type ?u.135168
α : Type u_4
β : Type ?u.135174
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
⊢ blockDiagonal 0 = 0
ext
no goals
case a.h
l : Type ?u.135132
m : Type u_1
n : Type u_2
o : Type u_3
p : Type ?u.135144
q : Type ?u.135147
m' : o → Type ?u.135152
n' : o → Type ?u.135157
p' : o → Type ?u.135162
R : Type ?u.135165
S : Type ?u.135168
α : Type u_4
β : Type ?u.135174
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
i✝ : m × o
x✝ : n × o
⊢ blockDiagonal 0 i✝ x✝ = OfNat.ofNat 0 i✝ x✝
simp [blockDiagonal_apply]