Of Gradient equivariant

lemma ofGradient_equivariant {d} (χ : SpaceTime d → ℝ) (hχ : Differentiable ℝ χ)    (Λ : LorentzGroup d) :    Λ • ofGradient χ = ofGradient (χ ∘ (Λ⁻¹ • ·)) := by  -- The metric-commutativity row identity, extracted from `comm_minkowskiMatrix`:  -- ∑ ν, Λ.1 μ ν * η ν κ = ∑ ν, η μ ν * (Λ⁻¹).1 κ ν  have hmetric : ∀ (μ κ : Fin 1 ⊕ Fin d),      ∑ ν, Λ.1 μ ν * η ν κ = ∑ ν, η μ ν * (Λ⁻¹).1 κ ν := by    intro μ κ    -- comm_minkowskiMatrix: Λ.1 * η = η * (Λ⁻¹)ᵀ, applied at (μ, κ)    have h := congr_fun₂ (LorentzGroup.comm_minkowskiMatrix (Λ := Λ)) μ κ    simp only [Matrix.mul_apply, LorentzGroup.transpose_val, Matrix.transpose_apply] at h    exact h  apply eq_of_val_eq; funext x μ  -- Let a κ = ∂_ κ χ (Λ⁻¹ • x). Both sides equal ∑ κ, (∑ ν, Λ.1 μ ν * η ν κ) * a κ.  set a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ (Λ⁻¹ • x)  -- Expand LHS: action_val → smul_eq_sum → ofGradient_apply_sum → reassociate + factor  have hlhs : (Λ • ofGradient χ).val x μ = ∑ κ, (∑ ν, Λ.1 μ ν * η ν κ) * a κ := by    simp only [ElectromagneticPotential.action_val, Lorentz.Vector.smul_eq_sum, a,      ofGradient_apply_sum, Finset.mul_sum]    rw [Finset.sum_comm]    apply Finset.sum_congr rfl; intro κ _    simp_rw [← mul_assoc]    rw [← Finset.sum_mul]  -- Expand RHS: ofGradient_apply_sum → deriv_comp_lorentz_action → sum_comm + factor + hmetric  have hrhs : (ofGradient (χ ∘ (Λ⁻¹ • ·))).val x μ = ∑ κ, (∑ ν, Λ.1 μ ν * η ν κ) * a κ := by    simp only [ofGradient_apply_sum, a]    conv_lhs =>      enter [2, ν]      rw [show ∂_ ν (χ ∘ (Λ⁻¹ • ·)) x = ∂_ ν (fun y => χ (Λ⁻¹ • y)) x from rfl,        SpaceTime.deriv_comp_lorentz_action ν χ hχ Λ⁻¹ x]    simp only [smul_eq_mul, Finset.mul_sum]    rw [Finset.sum_comm]    apply Finset.sum_congr rfl; intro κ _    simp_rw [← mul_assoc]    rw [← Finset.sum_mul, ← hmetric]  rw [hlhs, hrhs]