Grad Kinetic Term eq sum fderiv

lemma gradKineticTerm_eq_sum_fderiv {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)    (hA : ContDiff ℝ ∞ A) :    let F' : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d → ℝ) →    SpaceTime d → Lorentz.Vector d := fun μν => (fun ψ x =>    -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A x' μν.2) x)              (Lorentz.Vector.basis μν.1) •          Lorentz.Vector.basis μν.2 +        -(fderiv ℝ (fun x' => ∂_ μν.1 A x' μν.2 *          (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x)              (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 +      -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A x' μν.1) x) (Lorentz.Vector.basis μν.1) •        Lorentz.Vector.basis μν.2 +          -(fderiv ℝ (fun x' => ∂_ μν.1 A x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) •          Lorentz.Vector.basis μν.1))    A.gradKineticTerm 𝓕 = fun x => ∑ μν, F' μν (fun x' => -1/(2 * 𝓕.μ₀) * (fun _ => 1) x') x := by  apply HasVarGradientAt.varGradient  change HasVarGradientAt (fun A' x => ElectromagneticPotential.kineticTerm 𝓕 ⟨A'⟩ x) _ A  conv =>    enter [1, A', x]    rw [kineticTerm_eq_sum_potential]  let F : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d → Lorentz.Vector d) →    SpaceTime d → ℝ := fun (μ, ν) A' x =>        (η μ μ * η ν ν * ∂_ μ A' x ν ^ 2 - ∂_ μ A' x ν * ∂_ ν A' x μ)  have F_h (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) :=    HasVarAdjDerivAt.congr (G := F μν)      (HasVarAdjDerivAt.add _ _ _ _ _        (HasVarAdjDerivAt.const_mul _ _ A          (HasVarAdjDerivAt.mul _ _ _ _ A (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA)            (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA)) (c := η μν.1 μν.1 * η μν.2 μν.2))        (HasVarAdjDerivAt.neg _ _ A          (HasVarAdjDerivAt.mul _ _ _ _ A (deriv_hasVarAdjDerivAt μν.1 μν.2 A hA)            (deriv_hasVarAdjDerivAt μν.2 μν.1 A hA))))      (fun φ _ => funext fun x => by        simp [F]        ring)  have hF_mul := HasVarAdjDerivAt.const_mul _ _ A    (HasVarAdjDerivAt.congr (G := fun A' x => ∑ μ, ∑ ν, F (μ, ν) A' x)      (HasVarAdjDerivAt.sum _ _ A hA F_h)      (fun φ _ => funext fun x => Fintype.sum_prod_type fun μν => F μν φ x))    (c := -1/(2 * 𝓕.μ₀))  change HasVarGradientAt (fun A' x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, F (μ, ν) A' x) _ A  exact HasVarGradientAt.intro _ hF_mul rfl