Factor derivative identities on space-time products.

theorem CKN.spatialPartial_eq_joint_fderiv {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (z : Foundation.Parabolic.Vec3 × ℝ) (i : Fin 3) : spatialPartial (have this := g; this) i z = (fderiv ℝ g z) (basisVec i, 0)

theorem CKN.timePartial_eq_joint_fderiv {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (z : Foundation.Parabolic.Vec3 × ℝ) : timePartial (have this := g; this) z = (fderiv ℝ g z) (0, 1)