Harmonic Wave X electric Field space deriv same

lemma harmonicWaveX_electricField_space_deriv_same {d} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0)    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d.succ) :    Space.deriv i (fun x => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x i) x    = 0 := by  match i with  | 0 => simp [harmonicWaveX_electricField_zero]  | ⟨Nat.succ i, hi⟩ =>    have transverse_deriv_cos_eq_zero : ∀ (C a k b : ℝ) (l : Fin d) (y : Space d.succ),        Space.deriv l.succ (fun x => C * Real.cos (a - k * x 0 + b)) y = 0 := by      intro C a k b l y      rw [Space.deriv_eq, show (fun x : Space d.succ => C * Real.cos (a - k * x 0 + b))          = (fun u => C * Real.cos (a - k * u + b)) ∘ (fun x => x 0) from rfl,        fderiv_comp _ (by fun_prop) (by fun_prop)]      simp [← Space.deriv_eq, Space.deriv_component, Fin.succ_ne_zero]    rw [← Fin.succ_mk _ _ (by grind)]    conv_lhs =>      enter [2, x]      rw [harmonicWaveX_electricField_succ _ _ hk]    apply transverse_deriv_cos_eq_zero