Kinetic Term eq sum

lemma kineticTerm_eq_sum {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) :    A.kineticTerm 𝓕 x =    - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, ∑ μ', ∑ ν', η μ μ' * η ν ν' *      (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x) (μ, ν)      * (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr        (A.toFieldStrength x) (μ', ν') := by  rw [kineticTerm]  rw [toField_eq_repr]  rw [contrT_basis_repr_apply_eq_fin]  conv_lhs =>    enter [2, 2, μ]    rw [contrT_basis_repr_apply_eq_fin]    enter [2, ν]    rw [prodT_basis_repr_apply]    enter [1]    rw [contrT_basis_repr_apply_eq_fin]    enter [2, μ']    rw [contrT_basis_repr_apply_eq_fin]    enter [2, ν']    rw [prodT_basis_repr_apply]    enter [1]    rw [prodT_basis_repr_apply]    enter [1]    simp only [Tensorial.self_toTensor_apply]    rw [coMetric_repr_apply_eq_minkowskiMatrix]    change η μ' μ  conv_lhs =>    enter [2, 2, μ, 2, ν, 1, 2, μ', 2, ν', 1, 2]    simp only [Tensorial.self_toTensor_apply]    rw [coMetric_repr_apply_eq_minkowskiMatrix]    change η (ν') (ν)  conv_lhs =>    enter [2, 2, μ, 2, ν, 1, 2, μ', 2, ν', 2]    rw [toFieldStrength_tensor_basis_eq_basis]    change ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x))      (μ', ν')  conv_lhs =>    enter [2, 2, μ, 2, ν, 2]    rw [toFieldStrength_tensor_basis_eq_basis]    change ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x))      (μ, ν)  conv_lhs =>    enter [2, 2, μ]    enter [2, ν]    rw [Finset.sum_mul]    enter [2, μ']    rw [Finset.sum_mul]    enter [2, ν']    simp  conv_lhs => enter [2, 2, μ]; rw [Finset.sum_comm]  conv_lhs => rw [Finset.sum_comm]  conv_lhs => enter [2, 2, μ', 2, ν]; rw [Finset.sum_comm]  conv_lhs => enter [2, 2, μ']; rw [Finset.sum_comm]  rfl