Space Deriv momentum Flux component

lemma spaceDeriv_momentumFlux_component (d : ℕ) (fluid : FluidFlow d)    (t : Time) (x : Space d) (i j : Fin d)    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid t))    (hVelocity : Differentiable ℝ (fluid.velocity t)) :    ∂[j] (fun x' => momentumFlux d fluid t x' i j) x =      fluid.velocity t x i • ∂[j] (fun x' => momentumDensity d fluid t x' j) x +      ∂[j] (fun x' => fluid.velocity t x' i) x • momentumDensity d fluid t x j := by  have hProduct := Space.deriv_smul (u := j) (x := x)    (c := fun x' => fluid.velocity t x' i)    (f := fun x' => momentumDensity d fluid t x' j)    ((differentiable_euclidean.mp hVelocity i).differentiableAt)    ((differentiable_euclidean.mp hMomentumDensity j).differentiableAt)  rw [← hProduct]  congr  funext x'  simp [momentumFlux, momentumDensity, Matrix.vecMulVec_apply, mul_left_comm]