Matrix Div momentum Flux

lemma matrixDiv_momentumFlux (d : ℕ) (fluid : FluidFlow d)    (t : Time) (x : Space d)    (hMomentumDensity : Differentiable ℝ (momentumDensity d fluid t))    (hVelocity : Differentiable ℝ (fluid.velocity t)) :    matrixDiv d (momentumFlux d fluid t) x =      (∇ ⬝ momentumDensity d fluid t) x • fluid.velocity t x +        fluid.rho t x • convectiveTerm d fluid t x := by  ext i  simp [matrixDiv_apply, div, convectiveTerm, smul_eq_mul]  change (∑ j, ∂[j] (fun x' => momentumFlux d fluid t x' i j) x) =    (∑ j, ∂[j] (fun x' => momentumDensity d fluid t x' j) x) * fluid.velocity t x i +      fluid.rho t x * (∑ j, fluid.velocity t x j * ∂[j] (fluid.velocity t) x i)  calc    (∑ j, ∂[j] (fun x' => momentumFlux d fluid t x' i j) x)        = ∑ j,            (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          apply Finset.sum_congr rfl          intro j _          rw [spaceDeriv_momentumFlux_component d fluid t x i j            hMomentumDensity hVelocity]          simp [smul_eq_mul]    _ = fluid.velocity t x i * (∑ j, ∂[j] (fun x' => momentumDensity d fluid t x' j) x) +        fluid.rho t x * (∑ j, fluid.velocity t x j * ∂[j] (fluid.velocity t) x i) := by          rw [Finset.sum_add_distrib]          congr 1          · rw [Finset.mul_sum]          · rw [Finset.mul_sum]            apply Finset.sum_congr rfl            intro j _            rw [Space.deriv_euclid (ν := j) (μ := i) (f := fluid.velocity t)              hVelocity x]            simp [momentumDensity, mul_comm, mul_assoc]    _ = (∑ j, ∂[j] (fun x' => momentumDensity d fluid t x' j) x) * fluid.velocity t x i +        fluid.rho t x * (∑ j, fluid.velocity t x j * ∂[j] (fluid.velocity t) x i) := by          ring