no goals
l : Type ?u.46682
m : Type ?u.46685
n : Type u_1
o : Type ?u.46691
m' : o → Type ?u.46696
n' : o → Type ?u.46701
R : Type ?u.46704
S : Type ?u.46707
α : Type v
β : Type w
γ : Type ?u.46714
inst✝¹ : DecidableEq n
inst✝ : Zero α
d₁ d₂ : n → α
h : diagonal d₁ = diagonal d₂
i : n
⊢ d₁ i = d₂ i
simpa using congr_arg (fun m : Matrix n n α => m i i) h
no goals
l : Type ?u.46682
m : Type ?u.46685
n : Type u_1
o : Type ?u.46691
m' : o → Type ?u.46696
n' : o → Type ?u.46701
R : Type ?u.46704
S : Type ?u.46707
α : Type v
β : Type w
γ : Type ?u.46714
inst✝¹ : DecidableEq n
inst✝ : Zero α
d₁ d₂ : n → α
h : ∀ (i : n), d₁ i = d₂ i
⊢ diagonal d₁ = diagonal d₂
rw [show d₁ = d₂ from funext h]