Deriv has Var Adj Deriv At

lemma deriv_hasVarAdjDerivAt {d} (μ ν : Fin 1 ⊕ Fin d) (A : SpaceTime d → Lorentz.Vector d)    (hA : ContDiff ℝ ∞ A) :    HasVarAdjDerivAt (fun (A : SpaceTime d → Lorentz.Vector d) x => ∂_ μ A x ν)      (fun ψ x => - (fderiv ℝ ψ x) (Lorentz.Vector.basis μ) • Lorentz.Vector.basis ν) A := by  have h0' := HasVarAdjDerivAt.fderiv' _ _        (hF := hasVarAdjDerivAt_component ν A hA) A (Lorentz.Vector.basis μ)  refine HasVarAdjDerivAt.congr (G := (fun (A : SpaceTime d →    Lorentz.Vector d) x => ∂_ μ A x ν)) h0' ?_  intro φ hφ  funext x  rw [deriv_apply_eq μ ν φ]  exact hφ.differentiable (by simp)