∀ (R : Type u_3) {ι : Type u_2} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (M : Type u_1)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (i : ι) (x : ι → M)
  (hx : x ∈ MatrixModCat.toModuleCatObj R (ι → M) i),
  (fun x => ⟨Pi.single i x, ⋯⟩) ((fun x => ∑ i_1, ↑x i_1) ⟨x, hx⟩) = ⟨x, hx⟩