no goals
l : Type ?u.44950
m : Type ?u.44953
n : Type u_1
o : Type ?u.44959
m' : o → Type ?u.44964
n' : o → Type ?u.44969
R : Type ?u.44972
S : Type ?u.44975
α : Type v
β : Type w
γ : Type ?u.44982
inst✝¹ : DecidableEq n
inst✝ : Zero α
d : n → α
i : n
⊢ diagonal d i i = d i
simp [diagonal]