Harmonic Wave X is Plane Wave

lemma harmonicWaveX_isPlaneWave {d} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0)    (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) :    IsPlaneWave 𝓕 (harmonicWaveX 𝓕 k E₀ φ) ⟨Space.basis 0, by simp⟩ := by  apply And.intro  · use fun u => WithLp.toLp 2 fun i =>      match i with      | 0 => 0      | ⟨Nat.succ i, h⟩ => E₀ ⟨i, by grind⟩ * cos (-k * u + φ ⟨i, by grind⟩)    ext t x i    match i with    | 0 =>      simp [harmonicWaveX_electricField_zero, planeWave]      rfl    | ⟨Nat.succ i, h⟩ =>      simp only [Nat.succ_eq_add_one, neg_mul]      rw [← Fin.succ_mk _ _ (by grind)]      rw [harmonicWaveX_electricField_succ _ _ hk]      simp [planeWave]      left      ring_nf  · use fun u ij =>      match ij with      | (0, 0) => 0      | (0, ⟨Nat.succ j, hj⟩) =>        (- E₀ ⟨j, by grind⟩ / 𝓕.c.val) * cos (-k * u + φ ⟨j, by grind⟩)      | (⟨Nat.succ i, hi⟩, 0) =>        (E₀ ⟨i, by grind⟩ / 𝓕.c.val) * cos (-k * u + φ ⟨i, by grind⟩)      | (⟨Nat.succ i, hi⟩, ⟨Nat.succ j, hj⟩) => 0    intro t x    ext ij    match ij with    | (0, 0) =>      simp only [Nat.succ_eq_add_one, magneticFieldMatrix_diag_eq_zero, inner_basis, neg_mul]      rfl    | (⟨0, h0⟩, ⟨Nat.succ j, hj⟩) =>      simp only [Nat.succ_eq_add_one, Fin.zero_eta, inner_basis, neg_mul]      rw [← Fin.succ_mk _ _ (by grind)]      rw [harmonicWaveX_magneticFieldMatrix_zero_succ _ k hk]      simp only [Nat.succ_eq_add_one, mul_eq_mul_left_iff, div_eq_zero_iff, neg_eq_zero,        SpeedOfLight.val_ne_zero, or_false]      left      ring_nf    | (⟨Nat.succ i, hi⟩, ⟨0, h0⟩) =>      simp only [Nat.succ_eq_add_one, Fin.zero_eta, inner_basis, neg_mul]      rw [← Fin.succ_mk _ _ (by grind)]      rw [harmonicWaveX_magneticFieldMatrix_succ_zero _ k hk]      simp only [Nat.succ_eq_add_one, mul_eq_mul_left_iff, div_eq_zero_iff,        SpeedOfLight.val_ne_zero, or_false]      left      ring_nf    | (⟨Nat.succ i, hi⟩, ⟨Nat.succ j, hj⟩) =>      simp only [Nat.succ_eq_add_one]      rw [← Fin.succ_mk _ _ (by grind)]      rw [← Fin.succ_mk _ _ (by grind)]      rw [harmonicWaveX_magneticFieldMatrix_succ_succ _ _]