no goals
R : Type u_2
ι : Type u_3
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i j : ι
⊢ comp (proj i) (stdBasis R φ j) = diag j i
rw [stdBasis_eq_pi_diag, proj_pi]