no goals
l : Type ?u.210158
m : Type ?u.210161
n : Type ?u.210164
o : Type u_3
p : Type ?u.210170
q : Type ?u.210173
m' : o → Type u_1
n' : o → Type ?u.210183
p' : o → Type ?u.210188
R : Type ?u.210191
S : Type ?u.210194
α : Type u_2
β : Type ?u.210200
inst✝⁴ : DecidableEq o
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : (i : o) → DecidableEq (m' i)
inst✝ : One α
⊢ (blockDiagonal' fun i => diagonal fun x => 1) = diagonal fun x => 1
rw [blockDiagonal'_diagonal]