D Wirtinger Anti Dir comp

lemma dWirtingerAntiDir_comp {g : ℂ → ℂ} (hg : DifferentiableAt ℝ g (f u))    (hf : DifferentiableAt ℝ f u) (v : V) :    dWirtingerAntiDir (fun p => g (f p)) v u =      dWirtingerDir g 1 (f u) * dWirtingerAntiDir f v u        + dWirtingerAntiDir g 1 (f u) * dWirtingerAntiDir (fun p => star (f p)) v u := by  simp only [dWirtingerDir_apply, dWirtingerAntiDir_apply]  rw [show (fun p => g (f p)) = g ∘ f from rfl, fderiv_comp u hg hf, fderiv_star_eq hf]  simp only [ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe,    Complex.conjCLE_apply, Complex.star_def, smul_eq_mul, mul_one,    realLinear_apply_eq_wirtinger (fderiv ℝ g (f u)) (fderiv ℝ f u v),    realLinear_apply_eq_wirtinger (fderiv ℝ g (f u)) (fderiv ℝ f u (Complex.I • v))]  ring