Physlib.SpaceAndTime.Space.Translations

Physlib
SpaceAndTime
Space
Translations

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.SpaceAndTime.Space.Derivatives.Div

Translations on space

We define translations on space, and how translations act on distributions. Translations for part of the Poincaré group.

@[expose] public section

Translations of distributions

              @[simp]
lemma translateSchwartz_apply {d : ℕ} (a : EuclideanSpace ℝ (Fin d))
    (η : 𝓢(Space d, X)) (x : Space d) :
    translateSchwartz a η x = η (x - basis.repr.symm a) := rfllemma translateSchwartz_coe_eq {d : ℕ} (a : EuclideanSpace ℝ (Fin d))
    (η : 𝓢(Space d, X)) :
    (translateSchwartz a η : Space d → X) = fun x => η (x - basis.repr.symm a) := byX:Type u_3inst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)η:𝓢(Space d, X)⊢ ⇑((translateSchwartz a) η) = fun x => η (x - basis.repr.symm a)
  extX:Type u_3inst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)η:𝓢(Space d, X)x✝:Space d⊢ ((translateSchwartz a) η) x✝ = η (x✝ - basis.repr.symm a)
  simpAll goals completed! 🐙lemma distTranslate_apply {d : ℕ} (a : EuclideanSpace ℝ (Fin d))
    (T : (Space d) →d[ℝ] X) (η : 𝓢(Space d, ℝ)) :
    distTranslate a T η = T (translateSchwartz (-a) η) := rfl

@[simp]
lemma distTranslate_distGrad {d : ℕ} (a : EuclideanSpace ℝ (Fin d))
    (T : (Space d) →d[ℝ] ℝ) :
    distGrad (distTranslate a T) = distTranslate a (distGrad T) := byd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝ⊢ ∇ᵈ ((distTranslate a) T) = (distTranslate a) (∇ᵈ T)
  apply distGrad_eq_of_innerd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝ⊢ ∀ (η : 𝓢(Space d, ℝ)) (y : Space d),
  (((fderivD ℝ) ((distTranslate a) T)) η) y = ⟪((distTranslate a) (∇ᵈ T)) η, basis.repr y⟫_ℝ
  intro η yd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ (((fderivD ℝ) ((distTranslate a) T)) η) y = ⟪((distTranslate a) (∇ᵈ T)) η, basis.repr y⟫_ℝ
  rw [distTranslate_apply,d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ (((fderivD ℝ) ((distTranslate a) T)) η) y = ⟪(∇ᵈ T) ((translateSchwartz (-a)) η), basis.repr y⟫_ℝd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ (((fderivD ℝ) ((distTranslate a) T)) η) y =
  (((fderivD ℝ) T) ((translateSchwartz (-a)) η)) (basis.repr.symm (basis.repr y)) distGrad_inner_eqd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ (((fderivD ℝ) ((distTranslate a) T)) η) y =
  (((fderivD ℝ) T) ((translateSchwartz (-a)) η)) (basis.repr.symm (basis.repr y))d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ (((fderivD ℝ) ((distTranslate a) T)) η) y =
  (((fderivD ℝ) T) ((translateSchwartz (-a)) η)) (basis.repr.symm (basis.repr y))]d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ (((fderivD ℝ) ((distTranslate a) T)) η) y =
  (((fderivD ℝ) T) ((translateSchwartz (-a)) η)) (basis.repr.symm (basis.repr y))
  rw [fderivD_apply,d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ -((distTranslate a) T) ((SchwartzMap.evalCLM ℝ (Space d) ℝ y) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (((fderivD ℝ) T) ((translateSchwartz (-a)) η)) (basis.repr.symm (basis.repr y))d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ -T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ y) ((fderivCLM ℝ (Space d) ℝ) η))) =
  -T
      ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis.repr.symm (basis.repr y)))
        ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))) fderivD_apply,d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ -((distTranslate a) T) ((SchwartzMap.evalCLM ℝ (Space d) ℝ y) ((fderivCLM ℝ (Space d) ℝ) η)) =
  -T
      ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis.repr.symm (basis.repr y)))
        ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ -T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ y) ((fderivCLM ℝ (Space d) ℝ) η))) =
  -T
      ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis.repr.symm (basis.repr y)))
        ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))) distTranslate_applyd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ -T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ y) ((fderivCLM ℝ (Space d) ℝ) η))) =
  -T
      ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis.repr.symm (basis.repr y)))
        ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ -T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ y) ((fderivCLM ℝ (Space d) ℝ) η))) =
  -T
      ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis.repr.symm (basis.repr y)))
        ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))]d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ -T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ y) ((fderivCLM ℝ (Space d) ℝ) η))) =
  -T
      ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis.repr.symm (basis.repr y)))
        ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))
  congr 2e_6d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space d⊢ (translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ y) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis.repr.symm (basis.repr y)))
    ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))
  ext xe_6d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space dx:Space d⊢ ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ y) ((fderivCLM ℝ (Space d) ℝ) η))) x =
  ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis.repr.symm (basis.repr y)))
      ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))
    x
  simp only [translateSchwartz_apply, map_neg, sub_neg_eq_add,
    LinearIsometryEquiv.symm_apply_apply]e_6d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space dx:Space d⊢ ((SchwartzMap.evalCLM ℝ (Space d) ℝ y) ((fderivCLM ℝ (Space d) ℝ) η)) (x + basis.repr.symm a) =
  ((SchwartzMap.evalCLM ℝ (Space d) ℝ y) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))) x
  change fderiv ℝ η (x + basis.repr.symm a) y = fderiv ℝ _ x ye_6d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space dx:Space d⊢ (fderiv ℝ (⇑η) (x + basis.repr.symm a)) y = (fderiv ℝ (⇑((translateSchwartz (-a)) η)) x) y
  rw [translateSchwartz_coe_eqe_6d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space dx:Space d⊢ (fderiv ℝ (⇑η) (x + basis.repr.symm a)) y = (fderiv ℝ (fun x => η (x - basis.repr.symm (-a))) x) ye_6d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space dx:Space d⊢ (fderiv ℝ (⇑η) (x + basis.repr.symm a)) y = (fderiv ℝ (fun x => η (x - basis.repr.symm (-a))) x) y]e_6d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space dx:Space d⊢ (fderiv ℝ (⇑η) (x + basis.repr.symm a)) y = (fderiv ℝ (fun x => η (x - basis.repr.symm (-a))) x) y
  simp only [map_neg, sub_neg_eq_add]e_6d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space dx:Space d⊢ (fderiv ℝ (⇑η) (x + basis.repr.symm a)) y = (fderiv ℝ (fun x => η (x + basis.repr.symm a)) x) y
  rw [fderiv_comp_add_righte_6d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:Space dx:Space d⊢ (fderiv ℝ (⇑η) (x + basis.repr.symm a)) y = (fderiv ℝ (⇑η) (x + basis.repr.symm a)) yAll goals completed! 🐙]All goals completed! 🐙
lemma distTranslate_ofFunction {d : ℕ} (a : EuclideanSpace ℝ (Fin d))
    (f : Space d → X) (hf : IsDistBounded f) :
    distTranslate a (distOfFunction f hf) =
    distOfFunction (fun x => f (x - basis.repr.symm a))
    (IsDistBounded.comp_add_right hf (- basis.repr.symm a)) := byX:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded f⊢ (distTranslate a) (distOfFunction f hf) = distOfFunction (fun x => f (x - basis.repr.symm a)) ⋯
  ext ηX:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ((distTranslate a) (distOfFunction f hf)) η = (distOfFunction (fun x => f (x - basis.repr.symm a)) ⋯) η
  rw [distTranslate_apply,X:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ (distOfFunction f hf) ((translateSchwartz (-a)) η) = (distOfFunction (fun x => f (x - basis.repr.symm a)) ⋯) ηX:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x = ∫ (x : Space d), η x • f (x - basis.repr.symm a) distOfFunction_apply,X:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x = (distOfFunction (fun x => f (x - basis.repr.symm a)) ⋯) ηX:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x = ∫ (x : Space d), η x • f (x - basis.repr.symm a) distOfFunction_applyX:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x = ∫ (x : Space d), η x • f (x - basis.repr.symm a)X:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x = ∫ (x : Space d), η x • f (x - basis.repr.symm a)]X:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x = ∫ (x : Space d), η x • f (x - basis.repr.symm a)
  trans ∫ (x : Space d), η ((x - basis.repr.symm a) + basis.repr.symm a) •
    f (x - basis.repr.symm a)X:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x =
  ∫ (x : Space d), η (x - basis.repr.symm a + basis.repr.symm a) • f (x - basis.repr.symm a)X:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), η (x - basis.repr.symm a + basis.repr.symm a) • f (x - basis.repr.symm a) =
  ∫ (x : Space d), η x • f (x - basis.repr.symm a); swapX:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), η (x - basis.repr.symm a + basis.repr.symm a) • f (x - basis.repr.symm a) =
  ∫ (x : Space d), η x • f (x - basis.repr.symm a)X:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x =
  ∫ (x : Space d), η (x - basis.repr.symm a + basis.repr.symm a) • f (x - basis.repr.symm a)
  ·X:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), η (x - basis.repr.symm a + basis.repr.symm a) • f (x - basis.repr.symm a) =
  ∫ (x : Space d), η x • f (x - basis.repr.symm a) simpAll goals completed! 🐙
  let f' := fun x : Space d => η (x + basis.repr.symm a) • f (x)X:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)f':Space d → X := fun x => η (x + basis.repr.symm a) • f x⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x =
  ∫ (x : Space d), η (x - basis.repr.symm a + basis.repr.symm a) • f (x - basis.repr.symm a)
  change _ = ∫ (x : Space d), f' (x - basis.repr.symm a)X:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)f':Space d → X := fun x => η (x + basis.repr.symm a) • f x⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x = ∫ (x : Space d), f' (x - basis.repr.symm a)
  rw [MeasureTheory.integral_sub_right_eq_selfX:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)f':Space d → X := fun x => η (x + basis.repr.symm a) • f x⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x = ∫ (x : Space d), f' xX:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)f':Space d → X := fun x => η (x + basis.repr.symm a) • f x⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x = ∫ (x : Space d), f' x]X:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)f':Space d → X := fun x => η (x + basis.repr.symm a) • f x⊢ ∫ (x : Space d), ((translateSchwartz (-a)) η) x • f x = ∫ (x : Space d), f' x
  congre_fX:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)f':Space d → X := fun x => η (x + basis.repr.symm a) • f x⊢ (fun x => ((translateSchwartz (-a)) η) x • f x) = fun x => f' x
  funext xe_fX:Typeinst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕa:EuclideanSpace ℝ (Fin d)f:Space d → Xhf:IsDistBounded fη:𝓢(Space d, ℝ)f':Space d → X := fun x => η (x + basis.repr.symm a) • f xx:Space d⊢ ((translateSchwartz (-a)) η) x • f x = f' x
  simp [f']All goals completed! 🐙

@[simp]
lemma distDiv_distTranslate {d : ℕ} (a : EuclideanSpace ℝ (Fin d))
    (T : (Space d) →d[ℝ] EuclideanSpace ℝ (Fin d)) :
    distDiv (distTranslate a T) = distTranslate a (distDiv T) := byd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)⊢ distDiv ((distTranslate a) T) = (distTranslate a) (distDiv T)
  ext ηd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ (distDiv ((distTranslate a) T)) η = ((distTranslate a) (distDiv T)) η
  rw [distDiv_apply_eq_sum_fderivDd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) ((distTranslate a) T)) η) (basis i)).ofLp i = ((distTranslate a) (distDiv T)) ηd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) ((distTranslate a) T)) η) (basis i)).ofLp i = ((distTranslate a) (distDiv T)) η]d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) ((distTranslate a) T)) η) (basis i)).ofLp i = ((distTranslate a) (distDiv T)) η
  rw [distTranslate_apply,d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) ((distTranslate a) T)) η) (basis i)).ofLp i = (distDiv T) ((translateSchwartz (-a)) η)d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) ((distTranslate a) T)) η) (basis i)).ofLp i =
  ∑ i, ((((fderivD ℝ) T) ((translateSchwartz (-a)) η)) (basis i)).ofLp i distDiv_apply_eq_sum_fderivDd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) ((distTranslate a) T)) η) (basis i)).ofLp i =
  ∑ i, ((((fderivD ℝ) T) ((translateSchwartz (-a)) η)) (basis i)).ofLp id:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) ((distTranslate a) T)) η) (basis i)).ofLp i =
  ∑ i, ((((fderivD ℝ) T) ((translateSchwartz (-a)) η)) (basis i)).ofLp i]d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) ((distTranslate a) T)) η) (basis i)).ofLp i =
  ∑ i, ((((fderivD ℝ) T) ((translateSchwartz (-a)) η)) (basis i)).ofLp i
  congre_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ (fun i => ((((fderivD ℝ) ((distTranslate a) T)) η) (basis i)).ofLp i) = fun i =>
  ((((fderivD ℝ) T) ((translateSchwartz (-a)) η)) (basis i)).ofLp i
  funext ie_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin d⊢ ((((fderivD ℝ) ((distTranslate a) T)) η) (basis i)).ofLp i =
  ((((fderivD ℝ) T) ((translateSchwartz (-a)) η)) (basis i)).ofLp i
  rw [fderivD_apply,e_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin d⊢ (-((distTranslate a) T) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η))).ofLp i =
  ((((fderivD ℝ) T) ((translateSchwartz (-a)) η)) (basis i)).ofLp ie_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin d⊢ (-T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (-T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i fderivD_apply,e_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin d⊢ (-((distTranslate a) T) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η))).ofLp i =
  (-T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp ie_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin d⊢ (-T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (-T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i distTranslate_applye_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin d⊢ (-T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (-T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp ie_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin d⊢ (-T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (-T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i]e_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin d⊢ (-T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (-T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i
  simp only [PiLp.neg_apply, neg_inj]e_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin d⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i
  have h1 : ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i))
      ((fderivCLM ℝ (Space d) ℝ) η))) =
      ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i))
        ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))) := byd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)⊢ distDiv ((distTranslate a) T) = (distTranslate a) (distDiv T)e_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i
    ext xd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dx:Space d⊢ ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η))) x =
  ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))) xe_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i
    rw [translateSchwartz_applyd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dx:Space d⊢ ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) (x - basis.repr.symm (-a)) =
  ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))) xd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dx:Space d⊢ ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) (x - basis.repr.symm (-a)) =
  ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))) xe_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i]d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dx:Space d⊢ ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) (x - basis.repr.symm (-a)) =
  ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))) xe_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i
    simp only [map_neg, sub_neg_eq_add]d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dx:Space d⊢ ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) (x + basis.repr.symm a) =
  ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))) xe_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i
    change fderiv ℝ η (x + basis.repr.symm a) (basis i) = fderiv ℝ _ x (basis i)d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dx:Space d⊢ (fderiv ℝ (⇑η) (x + basis.repr.symm a)) (basis i) = (fderiv ℝ (⇑((translateSchwartz (-a)) η)) x) (basis i)e_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i
    rw [translateSchwartz_coe_eqd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dx:Space d⊢ (fderiv ℝ (⇑η) (x + basis.repr.symm a)) (basis i) = (fderiv ℝ (fun x => η (x - basis.repr.symm (-a))) x) (basis i)d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dx:Space d⊢ (fderiv ℝ (⇑η) (x + basis.repr.symm a)) (basis i) = (fderiv ℝ (fun x => η (x - basis.repr.symm (-a))) x) (basis i)e_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i]d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dx:Space d⊢ (fderiv ℝ (⇑η) (x + basis.repr.symm a)) (basis i) = (fderiv ℝ (fun x => η (x - basis.repr.symm (-a))) x) (basis i)e_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i
    simp only [map_neg, sub_neg_eq_add]d:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dx:Space d⊢ (fderiv ℝ (⇑η) (x + basis.repr.symm a)) (basis i) = (fderiv ℝ (fun x => η (x + basis.repr.symm a)) x) (basis i)e_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i
    rw [fderiv_comp_add_rightd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dx:Space d⊢ (fderiv ℝ (⇑η) (x + basis.repr.symm a)) (basis i) = (fderiv ℝ (⇑η) (x + basis.repr.symm a)) (basis i)e_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i]e_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp ie_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i
  rw [h1e_fd:ℕa:EuclideanSpace ℝ (Fin d)T:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)i:Fin dh1:(translateSchwartz (-a)) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) =
  (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η))⊢ (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp i =
  (T ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ((translateSchwartz (-a)) η)))).ofLp iAll goals completed! 🐙]All goals completed! 🐙