D Wirtinger Anti Coord eq complex fderiv apply

lemma dWirtingerAntiCoord_eq_complex_fderiv_apply {u : (ι → ℂ)}    (hg : DifferentiableAt ℂ g (star u)) (I : ι) :    dWirtingerAntiCoord (fun v : (ι → ℂ) => g (star v)) I u =      fderiv ℂ g (star u) (Pi.single I 1) := by  have hgr : DifferentiableAt ℝ g (conjCLM u) := hg.restrictScalars ℝ  change dWirtingerAntiDir (fun v : (ι → ℂ) => g (conjCLM v)) (Pi.single I 1) u      = fderiv ℂ g (star u) (Pi.single I 1)  rw [dWirtingerAntiDir_comp_conjLinear conjCLM_smul_I hgr]  simp only [conjCLM_apply, Pi.star_single, star_one]  rw [dWirtingerDir_eq_of_clinear (clinear_of_holomorphic hg _),    DifferentiableAt.fderiv_restrictScalars ℝ hg, ContinuousLinearMap.coe_restrictScalars']