no goals
l : Type ?u.47215
m : Type ?u.47218
n : Type u_1
o : Type ?u.47224
m' : o → Type ?u.47229
n' : o → Type ?u.47234
R : Type ?u.47237
S : Type ?u.47240
α : Type v
β : Type w
γ : Type ?u.47247
inst✝¹ : DecidableEq n
inst✝ : Zero α
d₁ d₂ : n → α
h : diagonal d₁ = diagonal d₂
i : n
⊢ d₁ i = d₂ i
simpa using Matrix.ext_iff.mpr h i i