Transverse Harmonic Plane Wave eq plane Wave

lemma transverseHarmonicPlaneWave_eq_planeWave {c : ℝ} {k : WaveVector} {f₀x f₀y ω δx δy : ℝ}    (hc_ge_zero : 0 < c) (hω_ge_zero : 0 < ω) (hk : k = EuclideanSpace.single 2 (ω/c)) :    (transverseHarmonicPlaneWave k f₀x f₀y ω δx δy hk) = planeWave    (fun p => (f₀x * Real.cos (-(ω/c)*p + δx)) • (EuclideanSpace.single 0 1) +    (f₀y * Real.cos (-(ω/c)*p + δy)) • (EuclideanSpace.single 1 1)) c    (WaveVector.toDirection k (by rw [hk]; simp [ne_of_gt, hc_ge_zero, hω_ge_zero])) := by  unfold transverseHarmonicPlaneWave planeWave  ext1 t  ext1 r  rw [harmonicWave, harmonicWave, WaveVector.toDirection]  simp only [Fin.isValue, neg_mul]  have normk: ‖k‖ = ω/c := by    rw [hk]    simp [← abs_div, hc_ge_zero, hω_ge_zero, le_of_lt]  rw [normk]  rw [mul_sub, inner_smul_right, real_inner_comm, ← mul_assoc]  ring_nf  simp [ne_of_gt, hc_ge_zero, hω_ge_zero, mul_comm ω, mul_assoc, basis_repr_inner_eq]