Cauchy Momentum Equation iff convective Cauchy Momentum Equation

lemma cauchyMomentumEquation_iff_convectiveCauchyMomentumEquation    (d : ℕ) (flow : CauchyFlow d)    (hContinuity : FluidFlow.ClassicalContinuityEquation d flow.toFluidFlow)    (hRhoTime : ∀ t x, DifferentiableAt ℝ (flow.rho · x) t)    (hVelocityTime : ∀ t x, DifferentiableAt ℝ (flow.velocity · x) t)    (hMomentumDensity : ∀ t, Differentiable ℝ (FluidFlow.momentumDensity d flow.toFluidFlow t))    (hVelocitySpace : ∀ t, Differentiable ℝ (flow.velocity t)) :    CauchyMomentumEquation d flow ↔ ConvectiveCauchyMomentumEquation d flow := by  have conservative_eq_convective_lhs : ∀ t x,      ∂ₜ (FluidFlow.momentumDensity d flow.toFluidFlow · x) t +          matrixDiv d (FluidFlow.momentumFlux d flow.toFluidFlow t) x =        flow.rho t x • FluidFlow.materialAcceleration d flow.toFluidFlow t x := by    intro t x    have hResidual : FluidFlow.continuityResidual d flow.toFluidFlow t x = 0 := by      simpa [FluidFlow.continuityResidual] using        hContinuity t x (by simpa using hRhoTime t x) (hMomentumDensity t).differentiableAt    rw [FluidFlow.momentumTransport_eq_materialAcceleration_add_continuityResidual        d flow.toFluidFlow t x (hRhoTime t x) (hVelocityTime t x)        (hMomentumDensity t) (hVelocitySpace t), hResidual, zero_smul, add_zero]  exact ⟨fun h t x => (conservative_eq_convective_lhs t x).symm.trans (h t x),    fun h t x => (conservative_eq_convective_lhs t x).trans (h t x)⟩