Harmonic Wave X magnetic Field Matrix space deriv succ

lemma harmonicWaveX_magneticFieldMatrix_space_deriv_succ {d} (𝓕 : FreeSpace) (k : ℝ)    (hk : k ≠ 0)    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) (t : Time) (x : Space d.succ)    (i j : Fin d.succ) (l : Fin d) :    Space.deriv l.succ (fun x => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x    = 0 := by  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]  match i, j with  | 0, 0 => simp  | ⟨Nat.succ i, hi⟩, ⟨Nat.succ j, hj⟩ =>    conv_lhs =>      enter [2, x]      rw [← Fin.succ_mk _ _ (by grind)]      rw [← Fin.succ_mk _ _ (by grind)]      rw [harmonicWaveX_magneticFieldMatrix_succ_succ _ _]    simp  | 0, ⟨Nat.succ j, hj⟩ =>    conv_lhs =>      enter [2, x]      rw [← Fin.succ_mk _ _ (by grind)]      rw [harmonicWaveX_magneticFieldMatrix_zero_succ _ k hk]    apply transverse_deriv_cos_eq_zero  | ⟨Nat.succ j, hj⟩, 0 =>    conv_lhs =>      enter [2, x]      rw [← Fin.succ_mk _ _ (by grind)]      rw [harmonicWaveX_magneticFieldMatrix_succ_zero _ k hk]    apply transverse_deriv_cos_eq_zero