Dist Deriv comp lorentz action

lemma distDeriv_comp_lorentz_action {μ : Fin 1 ⊕ Fin d} (Λ : LorentzGroup d)    (f : (SpaceTime d) →d[ℝ] M) :    distDeriv μ (Λ • f) = ∑ ν, Λ⁻¹.1 ν μ • (Λ • distDeriv ν f) := by  symm  trans (∑ ν, Λ • Λ⁻¹.1 ν μ • (distDeriv ν) f)  · congr    funext i    rw [SMulCommClass.smul_comm]  trans Λ • (∑ ν, Λ⁻¹.1 ν μ • (distDeriv ν) f)  · exact Eq.symm Finset.smul_sum  ext η  rw [lorentzGroup_smul_dist_apply, distDeriv_apply, fderivD_apply,    lorentzGroup_smul_dist_apply]  rw [← smul_neg]  congr  rw [_root_.sum_apply]  simp only [FunLike.coe_smul, Pi.smul_apply]  conv_lhs =>    enter [2, x]    rw [distDeriv_apply, fderivD_apply]    simp only [smul_neg]    rw [← map_smul]  rw [Finset.sum_neg_distrib]  congr  rw [← map_sum]  congr  /- Reduced to Schwartz maps -/  ext x  rw [_root_.sum_apply]  symm  simp [schwartzAction_apply]  change ∂_ μ η (Λ • x) = ∑ ν, Λ⁻¹.1 ν μ • ∂_ ν (schwartzAction Λ⁻¹ η) (x)  obtain ⟨η, rfl⟩ := schwartzAction_surjective Λ η  simp only [smul_eq_mul]  rw [schwartzAction_mul_apply]  simp only [inv_mul_cancel, map_one, one_apply_eq_self]  change ∂_ μ (fun x => η (Λ⁻¹ • x)) (Λ • x) = _  rw [deriv_comp_lorentz_action]  simp only [inv_smul_smul, smul_eq_mul]  exact SchwartzMap.differentiable η