To Field Strength action eq sum

lemma toFieldStrength_action_eq_sum {d} (A : ElectromagneticPotential d) (Λ : LorentzGroup d)    (hf : Differentiable ℝ A) (x : SpaceTime d) :    (Λ • A).toFieldStrength x = ∑ μ, ∑ ν,      (∑ κ, ∑ ρ, Λ.1 μ κ * Λ.1 ν ρ * toField {A.toFieldStrength (Λ⁻¹ • x) | [κ] [ρ]}ᵀ) •      Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν := by  conv_lhs => rw [toFieldStrength_equivariant A Λ hf x, toFieldStrength_eq_sum_basis_eval]  change Tensorial.smulLinearMap _ _ = _  simp only [map_sum, map_smul]  simp [smulLinearMap, smul_prod, Vector.smul_basis, tmul_sum, sum_tmul,    Finset.smul_sum, tmul_smul, smul_tmul, smul_smul]  conv_lhs => enter [2, μ, 2, ν]; rw [Finset.sum_comm]  conv_lhs => enter [2, μ]; rw [Finset.sum_comm]  rw [Finset.sum_comm]  refine Finset.sum_congr rfl (fun ν _ => ?_)  conv_lhs => enter [2, μ]; rw [Finset.sum_comm]  rw [Finset.sum_comm]  refine Finset.sum_congr rfl (fun μ _ => ?_)  simp [← Finset.sum_smul]  congr 1  exact Finset.sum_congr rfl (fun κ _ => Finset.sum_congr rfl (fun κ _ => by ring))