case a.h
k : Type ?u.9804
l : Type ?u.9807
m : Type ?u.9810
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i✝ x✝ : n
⊢ toMatrix (PEquiv.refl n) i✝ x✝ = OfNat.ofNat 1 i✝ x✝
k : Type ?u.9804
l : Type ?u.9807
m : Type ?u.9810
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
⊢ toMatrix (PEquiv.refl n) = 1
ext
no goals
case a.h
k : Type ?u.9804
l : Type ?u.9807
m : Type ?u.9810
n : Type u_1
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i✝ x✝ : n
⊢ toMatrix (PEquiv.refl n) i✝ x✝ = OfNat.ofNat 1 i✝ x✝
simp [toMatrix_apply, one_apply]