no goals
l : Type ?u.78390
m : Type ?u.78393
n : Type u_1
o : Type ?u.78399
m' : o → Type ?u.78404
n' : o → Type ?u.78409
R : Type ?u.78412
S : Type ?u.78415
α : Type v
β : Type w
γ : Type ?u.78422
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
⊢ OfNat.ofNat 1 i j = Pi.single i 1 j
simp only [one_apply, Pi.single_apply, eq_comm]