Grad Kinetic Term eq field Strength

lemma gradKineticTerm_eq_fieldStrength {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)    (x : SpaceTime d) (ha : ContDiff ℝ ∞ A) :    A.gradKineticTerm 𝓕 x = ∑ (ν : (Fin 1 ⊕ Fin d)), (1/𝓕.μ₀ * η ν ν) •    (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (A.fieldStrengthMatrix · (μ, ν)) x))    • Lorentz.Vector.basis ν := by  calc _    _ = ∑ (ν : (Fin 1 ⊕ Fin d)), ∑ (μ : (Fin 1 ⊕ Fin d)),      (1/𝓕.μ₀ * (η μ μ * η ν ν * ∂_ μ (fun x' => ∂_ μ A x' ν) x -      ∂_ μ (fun x' => ∂_ ν A x' μ) x)) • Lorentz.Vector.basis ν := by        rw [gradKineticTerm_eq_sum_sum A x ha]    _ = ∑ (ν : (Fin 1 ⊕ Fin d)), ∑ (μ : (Fin 1 ⊕ Fin d)),      ((1/𝓕.μ₀ * η ν ν) * (η μ μ * ∂_ μ (fun x' => ∂_ μ A x' ν) x -      η ν ν * ∂_ μ (fun x' => ∂_ ν A x' μ) x)) • Lorentz.Vector.basis ν := by        apply Finset.sum_congr rfl (fun ν _ => ?_)        apply Finset.sum_congr rfl (fun μ _ => ?_)        congr 1        ring_nf        simp    _ = ∑ (ν : (Fin 1 ⊕ Fin d)), ∑ (μ : (Fin 1 ⊕ Fin d)),      ((1/𝓕.μ₀ * η ν ν) * (∂_ μ (A.fieldStrengthMatrix · (μ, ν)) x)) •          Lorentz.Vector.basis ν := by        refine Finset.sum_congr rfl fun ν _ => Finset.sum_congr rfl fun μ _ => ?_        congr 2        conv_rhs =>          simp only [toFieldStrength_basis_repr_apply_eq_single]          rw [SpaceTime.deriv_eq, fderiv_fun_sub (by fun_prop) (by fun_prop),            fderiv_const_mul (by fun_prop), fderiv_const_mul (by fun_prop)]        simp [SpaceTime.deriv_eq]    _ = ∑ (ν : (Fin 1 ⊕ Fin d)), (1/𝓕.μ₀ * η ν ν) •        (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (A.fieldStrengthMatrix · (μ, ν)) x))        • Lorentz.Vector.basis ν := by        apply Finset.sum_congr rfl (fun ν _ => ?_)        rw [← Finset.sum_smul, ← Finset.mul_sum, ← smul_smul]