Rho coord sub center Of Mass

lemma rho_coord_sub_centerOfMass {d : ℕ} (R : RigidBody d) (h : R.mass ≠ 0) (j : Fin d) :    R.ρ (cmap (fun y => y j - R.centerOfMass j) (by fun_prop)) = 0 := by  have hsplit : cmap (fun y => y j - R.centerOfMass j) (by fun_prop)        = cmap (fun y => y j) (by fun_prop)          - R.centerOfMass j • (1 : C^⊤⟮𝓘(ℝ, Space d), Space d; 𝓘(ℝ, ℝ), ℝ⟯) := by    ext y    simp only [cmap_apply, ContMDiffMap.coe_sub, ContMDiffMap.coe_smul,      ContMDiffMap.coe_one, Pi.sub_apply, Pi.smul_apply, Pi.one_apply, smul_eq_mul, mul_one]  have hcoord : R.ρ (cmap (fun y => y j) (by fun_prop)) = R.mass * R.centerOfMass j := by    have hc : R.centerOfMass j = (1 / R.mass) • R.ρ (cmap (fun y => y j) (by fun_prop)) := rfl    rw [hc, smul_eq_mul, one_div, ← mul_assoc, mul_inv_cancel₀ h, one_mul]  rw [hsplit, map_sub, map_smul, R.rho_one, hcoord, smul_eq_mul]  ring