Spatial differentiation of the actual divergence forcing.

theorem AVenhance.Infra.Section4.amnrSpaceWord_coordinate_derivative {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (w : List (Fin 2)) (q : Fin 2) : (amnrSpaceWord w fun (x : Homogenization.Vec 2) => spaceGrad f x q) = fun (x : Homogenization.Vec 2) => spaceGrad (amnrSpaceWord w f) x q