D Wirtinger Anti Coord conj Coord

lemma dWirtingerAntiCoord_conjCoord (I J : ι) :    dWirtingerAntiCoord (fun u : (ι → ℂ) => star (u J)) I =      fun _ => if I = J then 1 else 0 := by  funext u  have hd : DifferentiableAt ℝ (fun w : (ι → ℂ) => w J) u :=    (ContinuousLinearMap.proj (R := ℝ) (φ := fun _ : ι => ℂ) J).differentiableAt  rw [show dWirtingerAntiCoord (fun u : (ι → ℂ) => star (u J)) I u      = star (dWirtingerCoord (fun w : (ι → ℂ) => w J) I u)      from dWirtingerAntiDir_star_comp hd (Pi.single I 1), dWirtingerCoord_coordProj]  simp only [apply_ite (star : ℂ → ℂ), star_one, star_zero]