Physlib.QuantumMechanics.Operators.Commutation — Physlib

Imports

/-
Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gregory J. Loges
-/
module

public import Physlib.Mathematics.KroneckerDelta.Basic
public import Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial
public import Physlib.QuantumMechanics.Operators.AngularMomentum

Commutation relations

i. Overview

In this module we compute the commutators for common operators acting on Schwartz maps on Space d.

Commutator lemmas come in three flavors:

a_commutation_b lemmas are of the form ⁅a, b⁆ = (⋯).

a_comp_b_commute and a_comp_commute lemmas are of the form a ∘ b = b ∘ a.

a_comp_b_eq lemmas are of the form a ∘ b = b ∘ a + (⋯).

ii. Key results

position_commutation_momentum : The canonical commutation relations.

angularMomentum_commutation_position : The position operator transforms as a vector under infinitessimal rotations.

angularMomentum_commutation_radiusRegPow : Functions of ‖x‖² commute with the angular momenta.

angularMomentum_commutation_momentum : The momentum operator transforms as a vector under infinitessimal rotations.

angularMomentum_commutation_angularMomentum : Angular momenta generate an 𝔰𝔬(d) algebra.

angularMomentumSqr_commutation_angularMomentum : 𝐋² is a quadratic Casimir of 𝔰𝔬(d).

iii. Table of contents

A. General

B. Commutators

B.1. Position / position

B.2. Momentum / momentum

B.3. Position / momentum

B.4. Angular momentum / position

B.5. Angular momentum / momentum

B.6. Angular momentum / angular momentum

iv. References

@[expose] public section

A. General

              lemma leibniz_lie (A B C : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) :
    ⁅A ∘L B, C⁆ = A ∘L ⁅B, C⁆ + ⁅A, C⁆ ∘L B := byd:ℕA:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)B:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)C:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)⊢ ⁅A ∘SL B, C⁆ = A ∘SL ⁅B, C⁆ + ⁅A, C⁆ ∘SL B
  dsimp only [Bracket.bracket]d:ℕA:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)B:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)C:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)⊢ A ∘SL B * C - C * A ∘SL B = A ∘SL (B * C - C * B) + (A * C - C * A) ∘SL B
  simp only [ContinuousLinearMap.mul_def, comp_assoc, comp_sub, sub_comp, sub_add_sub_cancel]All goals completed! 🐙lemma lie_leibniz (A B C : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) :
    ⁅A, B ∘L C⁆ = B ∘L ⁅A, C⁆ + ⁅A, B⁆ ∘L C := byd:ℕA:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)B:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)C:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)⊢ ⁅A, B ∘SL C⁆ = B ∘SL ⁅A, C⁆ + ⁅A, B⁆ ∘SL C
  dsimp only [Bracket.bracket]d:ℕA:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)B:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)C:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)⊢ A * B ∘SL C - B ∘SL C * A = B ∘SL (A * C - C * A) + (A * B - B * A) ∘SL C
  simp only [ContinuousLinearMap.mul_def, comp_assoc, comp_sub, sub_comp, sub_add_sub_cancel']All goals completed! 🐙lemma comp_eq_comp_add_commute (A B : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) :
    A ∘L B = B ∘L A + ⁅A, B⁆ := byd:ℕA:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)B:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)⊢ A ∘SL B = B ∘SL A + ⁅A, B⁆
  dsimp only [Bracket.bracket]d:ℕA:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)B:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)⊢ A ∘SL B = B ∘SL A + (A * B - B * A)
  simp only [ContinuousLinearMap.mul_def, add_sub_cancel]All goals completed! 🐙lemma comp_eq_comp_sub_commute (A B : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) :
    A ∘L B = B ∘L A - ⁅B, A⁆ := byd:ℕA:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)B:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)⊢ A ∘SL B = B ∘SL A - ⁅B, A⁆
  dsimp only [Bracket.bracket]d:ℕA:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)B:𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)⊢ A ∘SL B = B ∘SL A - (B * A - A * B)
  simp only [ContinuousLinearMap.mul_def, sub_sub_cancel]All goals completed! 🐙

B. Commutators

B.1. Position / position

Position operators commute: [xᵢ, xⱼ] = 0.

@[simp]
lemma position_commutation_position : ⁅𝐱 i, 𝐱 j⁆ = 0 := byd:ℕi:Fin dj:Fin d⊢ ⁅𝐱 i, 𝐱 j⁆ = 0
  extd:ℕi:Fin dj:Fin dx✝¹:𝓢(Space d, ℂ)x✝:Space d⊢ (⁅𝐱 i, 𝐱 j⁆ x✝¹) x✝ = (0 x✝¹) x✝
  simp [bracket, ← mul_assoc, mul_comm]All goals completed! 🐙

              

lemma position_comp_commute : 𝐱 i ∘L 𝐱 j = 𝐱 j ∘L 𝐱 i := byd:ℕi:Fin dj:Fin d⊢ 𝐱 i ∘SL 𝐱 j = 𝐱 j ∘SL 𝐱 i
  rw [comp_eq_comp_add_commute,d:ℕi:Fin dj:Fin d⊢ 𝐱 j ∘SL 𝐱 i + ⁅𝐱 i, 𝐱 j⁆ = 𝐱 j ∘SL 𝐱 iAll goals completed! 🐙 position_commutation_position,d:ℕi:Fin dj:Fin d⊢ 𝐱 j ∘SL 𝐱 i + 0 = 𝐱 j ∘SL 𝐱 iAll goals completed! 🐙 add_zerod:ℕi:Fin dj:Fin d⊢ 𝐱 j ∘SL 𝐱 i = 𝐱 j ∘SL 𝐱 iAll goals completed! 🐙]All goals completed! 🐙@[simp]
lemma position_commutation_radiusRegPow : ⁅𝐱 i, 𝐫₀[d] ε s⁆ = 0 := byd:ℕi:Fin dε:ℝˣs:ℝ⊢ ⁅𝐱 i, 𝐫₀ ε s⁆ = 0
  extd:ℕi:Fin dε:ℝˣs:ℝx✝¹:𝓢(Space d, ℂ)x✝:Space d⊢ (⁅𝐱 i, 𝐫₀ ε s⁆ x✝¹) x✝ = (0 x✝¹) x✝
  simp [bracket, ← mul_assoc, mul_comm]All goals completed! 🐙

lemma position_comp_radiusRegPow_commute : 𝐱 i ∘L 𝐫₀ ε s = 𝐫₀ ε s ∘L 𝐱 i := byd:ℕi:Fin dε:ℝˣs:ℝ⊢ 𝐱 i ∘SL 𝐫₀ ε s = 𝐫₀ ε s ∘SL 𝐱 i
  rw [comp_eq_comp_add_commute,d:ℕi:Fin dε:ℝˣs:ℝ⊢ 𝐫₀ ε s ∘SL 𝐱 i + ⁅𝐱 i, 𝐫₀ ε s⁆ = 𝐫₀ ε s ∘SL 𝐱 iAll goals completed! 🐙 position_commutation_radiusRegPow,d:ℕi:Fin dε:ℝˣs:ℝ⊢ 𝐫₀ ε s ∘SL 𝐱 i + 0 = 𝐫₀ ε s ∘SL 𝐱 iAll goals completed! 🐙 add_zerod:ℕi:Fin dε:ℝˣs:ℝ⊢ 𝐫₀ ε s ∘SL 𝐱 i = 𝐫₀ ε s ∘SL 𝐱 iAll goals completed! 🐙]All goals completed! 🐙@[simp]
lemma radiusRegPow_commutation_radiusRegPow : ⁅𝐫₀[d] ε s, 𝐫₀[d] ε t⁆ = 0 := byd:ℕε:ℝˣs:ℝt:ℝ⊢ ⁅𝐫₀ ε s, 𝐫₀ ε t⁆ = 0
  simp [bracket, mul_def, radiusRegPowCLM_comp_eq, add_comm]All goals completed! 🐙

B.2. Momentum / momentum

Momentum operators commute: [pᵢ, pⱼ] = 0.

@[simp]
lemma momentum_commutation_momentum : ⁅𝐩 i, 𝐩 j⁆ = 0 := byd:ℕi:Fin dj:Fin d⊢ ⁅𝐩 i, 𝐩 j⁆ = 0
  ext ψ xd:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ (⁅𝐩 i, 𝐩 j⁆ ψ) x = (0 ψ) x
  have hdiff (k : Fin d) : Differentiable ℝ (∂[k] ψ) := Space.deriv_differentiable (ψ.smooth 2) kd:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space dhdiff:∀ (k : Fin d), Differentiable ℝ (Space.deriv k ⇑ψ)⊢ (⁅𝐩 i, 𝐩 j⁆ ψ) x = (0 ψ) x
  show 𝐩 i (𝐩 j ψ) x - 𝐩 j (𝐩 i ψ) x = 0d:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space dhdiff:∀ (k : Fin d), Differentiable ℝ (Space.deriv k ⇑ψ)⊢ ((𝐩 i) ((𝐩 j) ψ)) x - ((𝐩 j) ((𝐩 i) ψ)) x = 0
  simp only [momentumCLM_apply_fun, Space.deriv_const_smul _ (hdiff _),
    Space.deriv_commute _ (ψ.smooth 2), sub_self]All goals completed! 🐙

              

lemma momentum_comp_commute : 𝐩 i ∘L 𝐩 j = 𝐩 j ∘L 𝐩 i := byd:ℕi:Fin dj:Fin d⊢ 𝐩 i ∘SL 𝐩 j = 𝐩 j ∘SL 𝐩 i
  rw [comp_eq_comp_add_commute,d:ℕi:Fin dj:Fin d⊢ 𝐩 j ∘SL 𝐩 i + ⁅𝐩 i, 𝐩 j⁆ = 𝐩 j ∘SL 𝐩 iAll goals completed! 🐙 momentum_commutation_momentum,d:ℕi:Fin dj:Fin d⊢ 𝐩 j ∘SL 𝐩 i + 0 = 𝐩 j ∘SL 𝐩 iAll goals completed! 🐙 add_zerod:ℕi:Fin dj:Fin d⊢ 𝐩 j ∘SL 𝐩 i = 𝐩 j ∘SL 𝐩 iAll goals completed! 🐙]All goals completed! 🐙attribute [local instance 100] LieRing.ofAssociativeRing@[simp]
lemma momentumSqr_commutation_momentum : ⁅𝐩[d] ⬝ᵥ 𝐩, 𝐩 i⁆ = 0 := byd:ℕi:Fin d⊢ ⁅𝐩 ⬝ᵥ 𝐩, 𝐩 i⁆ = 0
  simp [dotProduct, mul_def, sum_lie, leibniz_lie]All goals completed! 🐙

lemma momentumSqr_comp_momentum_commute : (𝐩 ⬝ᵥ 𝐩) ∘L 𝐩 i = 𝐩 i ∘L (𝐩 ⬝ᵥ 𝐩) := byd:ℕi:Fin d⊢ (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐩 i = 𝐩 i ∘SL (𝐩 ⬝ᵥ 𝐩)
  rw [comp_eq_comp_add_commute,d:ℕi:Fin d⊢ 𝐩 i ∘SL (𝐩 ⬝ᵥ 𝐩) + ⁅𝐩 ⬝ᵥ 𝐩, 𝐩 i⁆ = 𝐩 i ∘SL (𝐩 ⬝ᵥ 𝐩)All goals completed! 🐙 momentumSqr_commutation_momentum,d:ℕi:Fin d⊢ 𝐩 i ∘SL (𝐩 ⬝ᵥ 𝐩) + 0 = 𝐩 i ∘SL (𝐩 ⬝ᵥ 𝐩)All goals completed! 🐙 add_zerod:ℕi:Fin d⊢ 𝐩 i ∘SL (𝐩 ⬝ᵥ 𝐩) = 𝐩 i ∘SL (𝐩 ⬝ᵥ 𝐩)All goals completed! 🐙]All goals completed! 🐙

B.3. Position / momentum

The canonical commutation relations: [xᵢ, pⱼ] = iℏ δᵢⱼ𝟙.


lemma position_commutation_momentum : ⁅𝐱 i, 𝐩 j⁆ =
    (I * ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ) := byd:ℕi:Fin dj:Fin d⊢ ⁅𝐱 i, 𝐩 j⁆ = (I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)
  ext ψ xd:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ (⁅𝐱 i, 𝐩 j⁆ ψ) x = (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x
  show 𝐱 i (𝐩 j ψ) x - 𝐩 j (𝐱 i ψ) x = _d:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ ((𝐱 i) ((𝐩 j) ψ)) x - ((𝐩 j) ((𝐱 i) ψ)) x = (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x
  trans (I * ℏ) * (-x i * ∂[j] ψ x + ∂[j] ((fun x : Space d ↦ x i) • ⇑ψ) x)d:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ ((𝐱 i) ((𝐩 j) ψ)) x - ((𝐩 j) ((𝐱 i) ψ)) x =
  I * ↑↑ℏ * (-↑(x.val i) * Space.deriv j (⇑ψ) x + Space.deriv j ((fun x => x.val i) • ⇑ψ) x)d:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ I * ↑↑ℏ * (-↑(x.val i) * Space.deriv j (⇑ψ) x + Space.deriv j ((fun x => x.val i) • ⇑ψ) x) =
  (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x
  ·d:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ ((𝐱 i) ((𝐩 j) ψ)) x - ((𝐩 j) ((𝐱 i) ψ)) x =
  I * ↑↑ℏ * (-↑(x.val i) * Space.deriv j (⇑ψ) x + Space.deriv j ((fun x => x.val i) • ⇑ψ) x) simp only [positionCLM_apply, momentumCLM_apply, positionCLM_apply_fun]d:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ ↑(x.val i) * (-I * ↑↑ℏ * Space.deriv j (⇑ψ) x) - -I * ↑↑ℏ * Space.deriv j ((fun x => x.val i) • ⇑ψ) x =
  I * ↑↑ℏ * (-↑(x.val i) * Space.deriv j (⇑ψ) x + Space.deriv j ((fun x => x.val i) • ⇑ψ) x)
    ringAll goals completed! 🐙
  rw [Space.deriv_smul (byd:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ DifferentiableAt ℝ (fun x => x.val i) xd:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ I * ↑↑ℏ *
    (-↑(x.val i) * Space.deriv j (⇑ψ) x + (x.val i • Space.deriv j (⇑ψ) x + Space.deriv j (fun x => x.val i) x • ψ x)) =
  (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x fun_propAll goals completed! 🐙d:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ I * ↑↑ℏ *
    (-↑(x.val i) * Space.deriv j (⇑ψ) x + (x.val i • Space.deriv j (⇑ψ) x + Space.deriv j (fun x => x.val i) x • ψ x)) =
  (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x) (byd:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ DifferentiableAt ℝ (⇑ψ) xd:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ I * ↑↑ℏ *
    (-↑(x.val i) * Space.deriv j (⇑ψ) x + (x.val i • Space.deriv j (⇑ψ) x + Space.deriv j (fun x => x.val i) x • ψ x)) =
  (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x fun_propAll goals completed! 🐙d:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ I * ↑↑ℏ *
    (-↑(x.val i) * Space.deriv j (⇑ψ) x + (x.val i • Space.deriv j (⇑ψ) x + Space.deriv j (fun x => x.val i) x • ψ x)) =
  (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x)]d:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ I * ↑↑ℏ *
    (-↑(x.val i) * Space.deriv j (⇑ψ) x + (x.val i • Space.deriv j (⇑ψ) x + Space.deriv j (fun x => x.val i) x • ψ x)) =
  (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x
  rw [Space.deriv_componentd:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ I * ↑↑ℏ * (-↑(x.val i) * Space.deriv j (⇑ψ) x + (x.val i • Space.deriv j (⇑ψ) x + (if j = i then 1 else 0) • ψ x)) =
  (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) xd:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ I * ↑↑ℏ * (-↑(x.val i) * Space.deriv j (⇑ψ) x + (x.val i • Space.deriv j (⇑ψ) x + (if j = i then 1 else 0) • ψ x)) =
  (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x]d:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ I * ↑↑ℏ * (-↑(x.val i) * Space.deriv j (⇑ψ) x + (x.val i • Space.deriv j (⇑ψ) x + (if j = i then 1 else 0) • ψ x)) =
  (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x
  rcases eq_or_ne i j with (rfl | hne)inld:ℕi:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ I * ↑↑ℏ * (-↑(x.val i) * Space.deriv i (⇑ψ) x + (x.val i • Space.deriv i (⇑ψ) x + (if i = i then 1 else 0) • ψ x)) =
  (((I * ↑↑ℏ) • δ[i,i] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) xinrd:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space dhne:i ≠ j⊢ I * ↑↑ℏ * (-↑(x.val i) * Space.deriv j (⇑ψ) x + (x.val i • Space.deriv j (⇑ψ) x + (if j = i then 1 else 0) • ψ x)) =
  (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x
  ·inld:ℕi:Fin dψ:𝓢(Space d, ℂ)x:Space d⊢ I * ↑↑ℏ * (-↑(x.val i) * Space.deriv i (⇑ψ) x + (x.val i • Space.deriv i (⇑ψ) x + (if i = i then 1 else 0) • ψ x)) =
  (((I * ↑↑ℏ) • δ[i,i] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x simpAll goals completed! 🐙
  ·inrd:ℕi:Fin dj:Fin dψ:𝓢(Space d, ℂ)x:Space dhne:i ≠ j⊢ I * ↑↑ℏ * (-↑(x.val i) * Space.deriv j (⇑ψ) x + (x.val i • Space.deriv j (⇑ψ) x + (if j = i then 1 else 0) • ψ x)) =
  (((I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)) ψ) x simp [eq_zero_of_ne hne, hne.symm]All goals completed! 🐙

              

lemma momentum_comp_position_eq : 𝐩 j ∘L 𝐱 i =
    𝐱 i ∘L 𝐩 j - (I * ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ) := byd:ℕi:Fin dj:Fin d⊢ 𝐩 j ∘SL 𝐱 i = 𝐱 i ∘SL 𝐩 j - (I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)
  rw [comp_eq_comp_sub_commute,d:ℕi:Fin dj:Fin d⊢ 𝐱 i ∘SL 𝐩 j - ⁅𝐱 i, 𝐩 j⁆ = 𝐱 i ∘SL 𝐩 j - (I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)All goals completed! 🐙 position_commutation_momentumd:ℕi:Fin dj:Fin d⊢ 𝐱 i ∘SL 𝐩 j - (I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ) =
  𝐱 i ∘SL 𝐩 j - (I * ↑↑ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)All goals completed! 🐙]All goals completed! 🐙lemma position_position_commutation_momentum : ⁅𝐱 i ∘L 𝐱 j, 𝐩 k⁆ =
    (I * ℏ) • (δ[i,k] • 𝐱 j + δ[j,k] • 𝐱 i) := byd:ℕi:Fin dj:Fin dk:Fin d⊢ ⁅𝐱 i ∘SL 𝐱 j, 𝐩 k⁆ = (I * ↑↑ℏ) • (δ[i,k] • 𝐱 j + δ[j,k] • 𝐱 i)
  simp only [leibniz_lie, position_commutation_momentum, comp_smul, smul_comp, comp_id, id_comp,
    smul_add, add_comm]All goals completed! 🐙lemma position_commutation_momentum_momentum : ⁅𝐱 i, 𝐩 j ∘L 𝐩 k⁆ =
    (I * ℏ) • (δ[i,k] • 𝐩 j + δ[i,j] • 𝐩 k) := byd:ℕi:Fin dj:Fin dk:Fin d⊢ ⁅𝐱 i, 𝐩 j ∘SL 𝐩 k⁆ = (I * ↑↑ℏ) • (δ[i,k] • 𝐩 j + δ[i,j] • 𝐩 k)
  simp only [lie_leibniz, position_commutation_momentum, comp_smul, smul_comp, comp_id, id_comp,
    smul_add]All goals completed! 🐙lemma position_commutation_momentumSqr : ⁅𝐱 i, 𝐩 ⬝ᵥ 𝐩⁆ = (2 * I * ℏ) • 𝐩 i := byd:ℕi:Fin d⊢ ⁅𝐱 i, 𝐩 ⬝ᵥ 𝐩⁆ = (2 * I * ↑↑ℏ) • 𝐩 i
  simp only [dotProduct, mul_def, lie_sum, lie_leibniz, position_commutation_momentum, comp_smul,
    smul_comp, comp_id, id_comp, ← two_smul ℂ, smul_smul, mul_assoc, ← Finset.smul_sum, sum_smul]All goals completed! 🐙

lemma radiusRegPow_commutation_momentum :
    ⁅𝐫₀[d] ε s, 𝐩 i⁆ = (s * I * ℏ) • 𝐫₀ ε (s-2) ∘L 𝐱 i := byd:ℕi:Fin dε:ℝˣs:ℝ⊢ ⁅𝐫₀ ε s, 𝐩 i⁆ = (↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i
  ext ψ xd:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space d⊢ (⁅𝐫₀ ε s, 𝐩 i⁆ ψ) x = (((↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i) ψ) x
  have hne := Ne.symm (ne_of_lt <| Space.norm_sq_add_unit_sq_pos ε x)d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0⊢ (⁅𝐫₀ ε s, 𝐩 i⁆ ψ) x = (((↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i) ψ) x
  have hdiff1 : DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x := byd:ℕi:Fin dε:ℝˣs:ℝ⊢ ⁅𝐫₀ ε s, 𝐩 i⁆ = (↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 id:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x⊢ (⁅𝐫₀ ε s, 𝐩 i⁆ ψ) x = (((↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i) ψ) x
    refine DifferentiableAt.rpow_const ?_ (Or.intro_left _ hne)d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0⊢ DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) xd:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x⊢ (⁅𝐫₀ ε s, 𝐩 i⁆ ψ) x = (((↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i) ψ) x
    exact Differentiable.differentiableAt (byd:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0⊢ Differentiable ℝ fun x => ‖x‖ ^ 2 + ↑ε ^ 2d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x⊢ (⁅𝐫₀ ε s, 𝐩 i⁆ ψ) x = (((↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i) ψ) x fun_propAll goals completed! 🐙d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x⊢ (⁅𝐫₀ ε s, 𝐩 i⁆ ψ) x = (((↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i) ψ) x)d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x⊢ (⁅𝐫₀ ε s, 𝐩 i⁆ ψ) x = (((↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i) ψ) x
  have hdiff2 := Real.differentiableAt_rpow_const_of_ne (s / 2) hned:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)⊢ (⁅𝐫₀ ε s, 𝐩 i⁆ ψ) x = (((↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i) ψ) x
  have hdiff3 : DifferentiableAt ℝ (fun x ↦ ‖x‖ ^ 2 + ε ^ 2) x :=
    Differentiable.differentiableAt (byd:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)⊢ Differentiable ℝ fun x => ‖x‖ ^ 2 + ↑ε ^ 2d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (⁅𝐫₀ ε s, 𝐩 i⁆ ψ) x = (((↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i) ψ) x fun_propAll goals completed! 🐙d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (⁅𝐫₀ ε s, 𝐩 i⁆ ψ) x = (((↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i) ψ) x)d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (⁅𝐫₀ ε s, 𝐩 i⁆ ψ) x = (((↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i) ψ) x
  show 𝐫₀ ε s (𝐩 i ψ) x - 𝐩 i (𝐫₀ ε s ψ) x = (s * I * ℏ) * 𝐫₀ ε (s-2) (𝐱 i ψ) xd:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ ((𝐫₀ ε s) ((𝐩 i) ψ)) x - ((𝐩 i) ((𝐫₀ ε s) ψ)) x = ↑s * I * ↑↑ℏ * ((𝐫₀ ε (s - 2)) ((𝐱 i) ψ)) x
  simp only [momentumCLM_apply, positionCLM_apply, radiusRegPowCLM_apply_fun]d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • (-I * ↑↑ℏ * Space.deriv i (⇑ψ) x) -
    -I * ↑↑ℏ * Space.deriv i (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • ψ x) x =
  ↑s * I * ↑↑ℏ * (‖x‖ ^ 2 + ↑ε ^ 2) ^ ((s - 2) / 2) • (↑(x.val i) * ψ x)
  rw [← Pi.smul_def',d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • (-I * ↑↑ℏ * Space.deriv i (⇑ψ) x) -
    -I * ↑↑ℏ * Space.deriv i ((fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) • ⇑ψ) x =
  ↑s * I * ↑↑ℏ * (‖x‖ ^ 2 + ↑ε ^ 2) ^ ((s - 2) / 2) • (↑(x.val i) * ψ x)d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • (-I * ↑↑ℏ * Space.deriv i (⇑ψ) x) -
    -I * ↑↑ℏ *
      ((‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • Space.deriv i (⇑ψ) x +
        Space.deriv i (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x • ψ x) =
  ↑s * I * ↑↑ℏ * (‖x‖ ^ 2 + ↑ε ^ 2) ^ ((s - 2) / 2) • (↑(x.val i) * ψ x) Space.deriv_smul hdiff1 (byd:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ DifferentiableAt ℝ (⇑ψ) xd:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • (-I * ↑↑ℏ * Space.deriv i (⇑ψ) x) -
    -I * ↑↑ℏ *
      ((‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • Space.deriv i (⇑ψ) x +
        Space.deriv i (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x • ψ x) =
  ↑s * I * ↑↑ℏ * (‖x‖ ^ 2 + ↑ε ^ 2) ^ ((s - 2) / 2) • (↑(x.val i) * ψ x) fun_propAll goals completed! 🐙d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • (-I * ↑↑ℏ * Space.deriv i (⇑ψ) x) -
    -I * ↑↑ℏ *
      ((‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • Space.deriv i (⇑ψ) x +
        Space.deriv i (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x • ψ x) =
  ↑s * I * ↑↑ℏ * (‖x‖ ^ 2 + ↑ε ^ 2) ^ ((s - 2) / 2) • (↑(x.val i) * ψ x))]d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • (-I * ↑↑ℏ * Space.deriv i (⇑ψ) x) -
    -I * ↑↑ℏ *
      ((‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • Space.deriv i (⇑ψ) x +
        Space.deriv i (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x • ψ x) =
  ↑s * I * ↑↑ℏ * (‖x‖ ^ 2 + ↑ε ^ 2) ^ ((s - 2) / 2) • (↑(x.val i) * ψ x)
  suffices ∂[i] (fun x ↦ (‖x‖ ^ 2 + ε ^ 2) ^ (s / 2)) x =
      s * (‖x‖ ^ 2 + ε ^ 2) ^ (s / 2 - 1) * x i byd:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) xthis:Space.deriv i (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x = s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val i⊢ (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • (-I * ↑↑ℏ * Space.deriv i (⇑ψ) x) -
    -I * ↑↑ℏ *
      ((‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • Space.deriv i (⇑ψ) x +
        Space.deriv i (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x • ψ x) =
  ↑s * I * ↑↑ℏ * (‖x‖ ^ 2 + ↑ε ^ 2) ^ ((s - 2) / 2) • (↑(x.val i) * ψ x)d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ Space.deriv i (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x = s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val i
    simp only [this, real_smul, ofReal_mul]d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) xthis:Space.deriv i (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x = s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val i⊢ ↑((‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) * (-I * ↑↑ℏ * Space.deriv i (⇑ψ) x) -
    -I * ↑↑ℏ *
      (↑((‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) * Space.deriv i (⇑ψ) x +
        ↑s * ↑((‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1)) * ↑(x.val i) * ψ x) =
  ↑s * I * ↑↑ℏ * (↑((‖x‖ ^ 2 + ↑ε ^ 2) ^ ((s - 2) / 2)) * (↑(x.val i) * ψ x))d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ Space.deriv i (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x = s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val i
    ring_nfd:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ Space.deriv i (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x = s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val id:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ Space.deriv i (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) x = s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val i
  change ∂[i] ((fun r ↦ r ^ (s / 2)) ∘ (fun x ↦ ‖x‖ ^ 2 + ε ^ 2)) x = _d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ Space.deriv i ((fun r => r ^ (s / 2)) ∘ fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x = s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val i
  rw [Space.deriv_eq,d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (fderiv ℝ ((fun r => r ^ (s / 2)) ∘ fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x) (Space.basis i) =
  s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val id:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (fderiv ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2) ∘SL (2 • (innerSL ℝ) x)) (Space.basis i) =
  s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val i fderiv_comp x hdiff2 hdiff3,d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (fderiv ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2) ∘SL fderiv ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x) (Space.basis i) =
  s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val id:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (fderiv ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2) ∘SL (2 • (innerSL ℝ) x)) (Space.basis i) =
  s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val i fderiv_add_const,d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (fderiv ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2) ∘SL fderiv ℝ (fun x => ‖x‖ ^ 2) x) (Space.basis i) =
  s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val id:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (fderiv ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2) ∘SL (2 • (innerSL ℝ) x)) (Space.basis i) =
  s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val i fderiv_norm_sq_applyd:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (fderiv ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2) ∘SL (2 • (innerSL ℝ) x)) (Space.basis i) =
  s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val id:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (fderiv ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2) ∘SL (2 • (innerSL ℝ) x)) (Space.basis i) =
  s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val i]d:ℕi:Fin dε:ℝˣs:ℝψ:𝓢(Space d, ℂ)x:Space dhne:‖x‖ ^ 2 + ↑ε ^ 2 ≠ 0hdiff1:DifferentiableAt ℝ (fun x => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2)) xhdiff2:DifferentiableAt ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2)hdiff3:DifferentiableAt ℝ (fun x => ‖x‖ ^ 2 + ↑ε ^ 2) x⊢ (fderiv ℝ (fun x => x ^ (s / 2)) (‖x‖ ^ 2 + ↑ε ^ 2) ∘SL (2 • (innerSL ℝ) x)) (Space.basis i) =
  s * (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2 - 1) * x.val i
  simp [Real.deriv_rpow_const, mul_comm, ← mul_assoc, mul_div_cancel₀ s (NeZero.ne' 2).symm]All goals completed! 🐙

lemma momentum_comp_radiusRegPow_eq :
    𝐩 i ∘L 𝐫₀ ε s = 𝐫₀ ε s ∘L 𝐩 i - (s * I * ℏ) • 𝐫₀ ε (s-2) ∘L 𝐱 i := byd:ℕi:Fin dε:ℝˣs:ℝ⊢ 𝐩 i ∘SL 𝐫₀ ε s = 𝐫₀ ε s ∘SL 𝐩 i - (↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i
  rw [comp_eq_comp_sub_commute,d:ℕi:Fin dε:ℝˣs:ℝ⊢ 𝐫₀ ε s ∘SL 𝐩 i - ⁅𝐫₀ ε s, 𝐩 i⁆ = 𝐫₀ ε s ∘SL 𝐩 i - (↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 iAll goals completed! 🐙 radiusRegPow_commutation_momentumd:ℕi:Fin dε:ℝˣs:ℝ⊢ 𝐫₀ ε s ∘SL 𝐩 i - (↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 i = 𝐫₀ ε s ∘SL 𝐩 i - (↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL 𝐱 iAll goals completed! 🐙]All goals completed! 🐙lemma radiusRegPow_commutation_momentumSqr :
    ⁅𝐫₀[d] ε s, 𝐩[d] ⬝ᵥ 𝐩⁆ = (2 * s * I * ℏ) • 𝐫₀ ε (s-2) ∘L (𝐱 ⬝ᵥ 𝐩)
    + (s * (d + s - 2) * ℏ ^ 2) • 𝐫₀ ε (s-2) - (ε ^ 2 * s * (s - 2) * ℏ ^ 2) • 𝐫₀ ε (s-4) := byd:ℕε:ℝˣs:ℝ⊢ ⁅𝐫₀ ε s, 𝐩 ⬝ᵥ 𝐩⁆ =
  (2 * ↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) + (s * (↑d + s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 2) -
    (↑ε ^ 2 * s * (s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 4)
  calc
    _ = (s * I * ℏ) • ∑ i, ((𝐩 i ∘L 𝐫₀ ε (s-2)) ∘L 𝐱 i + 𝐫₀ ε (s-2) ∘L 𝐱 i ∘L 𝐩 i) := byd:ℕε:ℝˣs:ℝ⊢ ⁅𝐫₀ ε s, 𝐩 ⬝ᵥ 𝐩⁆ = (↑s * I * ↑↑ℏ) • ∑ i, ((𝐩 i ∘SL 𝐫₀ ε (s - 2)) ∘SL 𝐱 i + 𝐫₀ ε (s - 2) ∘SL 𝐱 i ∘SL 𝐩 i)
      simp [dotProduct, mul_def, lie_sum, lie_leibniz, radiusRegPow_commutation_momentum,
        ← smul_add, ← Finset.smul_sum, comp_assoc]All goals completed! 🐙
    _ = (s * I * ℏ) • ∑ i, (𝐫₀ ε (s-2) ∘L 𝐩 i ∘L 𝐱 i + 𝐫₀ ε (s-2) ∘L 𝐱 i ∘L 𝐩 i
        - (↑(s - 2) * I * ℏ) • 𝐫₀ ε (s-4) ∘L 𝐱 i ∘L 𝐱 i) := byd:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ) • ∑ i, ((𝐩 i ∘SL 𝐫₀ ε (s - 2)) ∘SL 𝐱 i + 𝐫₀ ε (s - 2) ∘SL 𝐱 i ∘SL 𝐩 i) =
  (↑s * I * ↑↑ℏ) •
    ∑ i,
      (𝐫₀ ε (s - 2) ∘SL 𝐩 i ∘SL 𝐱 i + 𝐫₀ ε (s - 2) ∘SL 𝐱 i ∘SL 𝐩 i -
        (↑(s - 2) * I * ↑↑ℏ) • 𝐫₀ ε (s - 4) ∘SL 𝐱 i ∘SL 𝐱 i)
      simp only [momentum_comp_radiusRegPow_eq, sub_comp, smul_comp, sub_add_eq_add_sub, comp_assoc]d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ) •
    ∑ x,
      (𝐫₀ ε (s - 2) ∘SL 𝐩 x ∘SL 𝐱 x + 𝐫₀ ε (s - 2) ∘SL 𝐱 x ∘SL 𝐩 x -
        (↑(s - 2) * I * ↑↑ℏ) • 𝐫₀ ε (s - 2 - 2) ∘SL 𝐱 x ∘SL 𝐱 x) =
  (↑s * I * ↑↑ℏ) •
    ∑ i,
      (𝐫₀ ε (s - 2) ∘SL 𝐩 i ∘SL 𝐱 i + 𝐫₀ ε (s - 2) ∘SL 𝐱 i ∘SL 𝐩 i -
        (↑(s - 2) * I * ↑↑ℏ) • 𝐫₀ ε (s - 4) ∘SL 𝐱 i ∘SL 𝐱 i)
      ring_nfAll goals completed! 🐙
    _ = (s * I * ℏ) • ∑ i, ((2 : ℂ) • 𝐫₀ ε (s-2) ∘L 𝐱 i ∘L 𝐩 i - (I * ℏ) • 𝐫₀ ε (s-2)
        - ((s - 2) * I * ℏ) • 𝐫₀ ε (s-4) ∘L 𝐱 i ∘L 𝐱 i) := byd:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ) •
    ∑ i,
      (𝐫₀ ε (s - 2) ∘SL 𝐩 i ∘SL 𝐱 i + 𝐫₀ ε (s - 2) ∘SL 𝐱 i ∘SL 𝐩 i -
        (↑(s - 2) * I * ↑↑ℏ) • 𝐫₀ ε (s - 4) ∘SL 𝐱 i ∘SL 𝐱 i) =
  (↑s * I * ↑↑ℏ) •
    ∑ i,
      (2 • 𝐫₀ ε (s - 2) ∘SL 𝐱 i ∘SL 𝐩 i - (I * ↑↑ℏ) • 𝐫₀ ε (s - 2) -
        ((↑s - 2) * I * ↑↑ℏ) • 𝐫₀ ε (s - 4) ∘SL 𝐱 i ∘SL 𝐱 i)
      simp [momentum_comp_position_eq, sub_add_eq_add_sub, ← two_smul ℂ]All goals completed! 🐙
    _ = (s * I * ℏ) • ((2 : ℂ) • 𝐫₀ ε (s-2) ∘L (𝐱 ⬝ᵥ 𝐩) - (d * I * ℏ) • 𝐫₀ ε (s-2)
        - ((s - 2) * I * ℏ) • 𝐫₀ ε (s-4) ∘L ∑ i, 𝐱 i ∘L 𝐱 i) := byd:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ) •
    ∑ i,
      (2 • 𝐫₀ ε (s - 2) ∘SL 𝐱 i ∘SL 𝐩 i - (I * ↑↑ℏ) • 𝐫₀ ε (s - 2) -
        ((↑s - 2) * I * ↑↑ℏ) • 𝐫₀ ε (s - 4) ∘SL 𝐱 i ∘SL 𝐱 i) =
  (↑s * I * ↑↑ℏ) •
    (2 • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) - (↑d * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) -
      ((↑s - 2) * I * ↑↑ℏ) • 𝐫₀ ε (s - 4) ∘SL ∑ i, 𝐱 i ∘SL 𝐱 i)
      simp [Finset.sum_sub_distrib, ← Finset.smul_sum, ← comp_finsetSum,
        ← Nat.cast_smul_eq_nsmul ℂ, smul_smul, dotProduct, mul_def, mul_assoc]All goals completed! 🐙
    _ = (2 * s * I * ℏ) • 𝐫₀ ε (s-2) ∘L (𝐱 ⬝ᵥ 𝐩) + (s * (d + s - 2) * ℏ ^ 2) • 𝐫₀ ε (s-2)
        - (ε ^ 2 * s * (s - 2) * ℏ ^ 2) • 𝐫₀ ε (s-4) := byd:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ) •
    (2 • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) - (↑d * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) -
      ((↑s - 2) * I * ↑↑ℏ) • 𝐫₀ ε (s - 4) ∘SL ∑ i, 𝐱 i ∘SL 𝐱 i) =
  (2 * ↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) + (s * (↑d + s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 2) -
    (↑ε ^ 2 * s * (s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 4)
      simp_rw [d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ) •
    (2 • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) - (↑d * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) -
      ((↑s - 2) * I * ↑↑ℏ) • 𝐫₀ ε (s - 4) ∘SL ∑ i, 𝐱 i ∘SL 𝐱 i) =
  (2 * ↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) + (s * (↑d + s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 2) -
    (↑ε ^ 2 * s * (s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 4)positionSqCLM_eq ε,d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ) •
    (2 • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) - (↑d * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) -
      ((↑s - 2) * I * ↑↑ℏ) • 𝐫₀ ε (s - 4) ∘SL (𝐫₀ ε 2 - ↑ε ^ 2 • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ))) =
  (2 * ↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) + (s * (↑d + s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 2) -
    (↑ε ^ 2 * s * (s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 4) comp_sub,d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ) •
    (2 • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) - (↑d * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) -
      ((↑s - 2) * I * ↑↑ℏ) •
        (𝐫₀ ε (s - 4) ∘SL 𝐫₀ ε 2 - 𝐫₀ ε (s - 4) ∘SL (↑ε ^ 2 • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ)))) =
  (2 * ↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) + (s * (↑d + s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 2) -
    (↑ε ^ 2 * s * (s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 4) comp_smul,d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ) •
    (2 • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) - (↑d * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) -
      ((↑s - 2) * I * ↑↑ℏ) •
        (𝐫₀ ε (s - 4) ∘SL 𝐫₀ ε 2 - ↑ε ^ 2 • 𝐫₀ ε (s - 4) ∘SL ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ))) =
  (2 * ↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) + (s * (↑d + s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 2) -
    (↑ε ^ 2 * s * (s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 4) comp_id,d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ) •
    (2 • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) - (↑d * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) -
      ((↑s - 2) * I * ↑↑ℏ) • (𝐫₀ ε (s - 4) ∘SL 𝐫₀ ε 2 - ↑ε ^ 2 • 𝐫₀ ε (s - 4))) =
  (2 * ↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) + (s * (↑d + s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 2) -
    (↑ε ^ 2 * s * (s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 4) radiusRegPowCLM_comp_eqd:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ) •
    (2 • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) - (↑d * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) -
      ((↑s - 2) * I * ↑↑ℏ) • (𝐫₀ ε (s - 4 + 2) - ↑ε ^ 2 • 𝐫₀ ε (s - 4))) =
  (2 * ↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) + (s * (↑d + s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 2) -
    (↑ε ^ 2 * s * (s - 2) * ↑ℏ ^ 2) • 𝐫₀ ε (s - 4)]
      simp only [smul_sub, smul_smul, ← Complex.coe_smul, ofReal_mul, ofReal_add, ofReal_sub,
        ofReal_pow, ofReal_ofNat, ofReal_natCast]d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) - (↑s * I * ↑↑ℏ * (↑d * I * ↑↑ℏ)) • 𝐫₀ ε (s - 2) -
    ((↑s * I * ↑↑ℏ * ((↑s - 2) * I * ↑↑ℏ)) • 𝐫₀ ε (s - 4 + 2) -
      (↑s * I * ↑↑ℏ * ((↑s - 2) * I * ↑↑ℏ * ↑↑ε ^ 2)) • 𝐫₀ ε (s - 4)) =
  (2 * ↑s * I * ↑↑ℏ) • 𝐫₀ ε (s - 2) ∘SL (𝐱 ⬝ᵥ 𝐩) + (↑s * (↑d + ↑s - 2) * ↑↑ℏ ^ 2) • 𝐫₀ ε (s - 2) -
    (↑↑ε ^ 2 * ↑s * (↑s - 2) * ↑↑ℏ ^ 2) • 𝐫₀ ε (s - 4)
      ring_nfd:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) - (↑s * I ^ 2 * ↑↑ℏ ^ 2 * ↑d) • 𝐫₀ ε (-2 + s) -
    ((-(↑s * I ^ 2 * ↑↑ℏ ^ 2 * 2) + ↑s ^ 2 * I ^ 2 * ↑↑ℏ ^ 2) • 𝐫₀ ε (-2 + s) -
      (-(↑s * I ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * I ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s)) =
  (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) +
      (-(↑s * ↑↑ℏ ^ 2 * 2) + ↑s * ↑↑ℏ ^ 2 * ↑d + ↑s ^ 2 * ↑↑ℏ ^ 2) • 𝐫₀ ε (-2 + s) -
    (-(↑s * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s)
      simp_rw [d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) - (↑s * I ^ 2 * ↑↑ℏ ^ 2 * ↑d) • 𝐫₀ ε (-2 + s) -
    ((-(↑s * I ^ 2 * ↑↑ℏ ^ 2 * 2) + ↑s ^ 2 * I ^ 2 * ↑↑ℏ ^ 2) • 𝐫₀ ε (-2 + s) -
      (-(↑s * I ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * I ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s)) =
  (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) +
      (-(↑s * ↑↑ℏ ^ 2 * 2) + ↑s * ↑↑ℏ ^ 2 * ↑d + ↑s ^ 2 * ↑↑ℏ ^ 2) • 𝐫₀ ε (-2 + s) -
    (-(↑s * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s)← sub_add,d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) - (↑s * I ^ 2 * ↑↑ℏ ^ 2 * ↑d) • 𝐫₀ ε (-2 + s) -
      (-(↑s * I ^ 2 * ↑↑ℏ ^ 2 * 2) + ↑s ^ 2 * I ^ 2 * ↑↑ℏ ^ 2) • 𝐫₀ ε (-2 + s) +
    (-(↑s * I ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * I ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s) =
  (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) +
      (-(↑s * ↑↑ℏ ^ 2 * 2) + ↑s * ↑↑ℏ ^ 2 * ↑d + ↑s ^ 2 * ↑↑ℏ ^ 2) • 𝐫₀ ε (-2 + s) -
    (-(↑s * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s) sub_sub,d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) -
      ((↑s * I ^ 2 * ↑↑ℏ ^ 2 * ↑d) • 𝐫₀ ε (-2 + s) +
        (-(↑s * I ^ 2 * ↑↑ℏ ^ 2 * 2) + ↑s ^ 2 * I ^ 2 * ↑↑ℏ ^ 2) • 𝐫₀ ε (-2 + s)) +
    (-(↑s * I ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * I ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s) =
  (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) +
      (-(↑s * ↑↑ℏ ^ 2 * 2) + ↑s * ↑↑ℏ ^ 2 * ↑d + ↑s ^ 2 * ↑↑ℏ ^ 2) • 𝐫₀ ε (-2 + s) -
    (-(↑s * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s) ← add_smul,d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) -
      (↑s * I ^ 2 * ↑↑ℏ ^ 2 * ↑d + (-(↑s * I ^ 2 * ↑↑ℏ ^ 2 * 2) + ↑s ^ 2 * I ^ 2 * ↑↑ℏ ^ 2)) • 𝐫₀ ε (-2 + s) +
    (-(↑s * I ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * I ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s) =
  (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) +
      (-(↑s * ↑↑ℏ ^ 2 * 2) + ↑s * ↑↑ℏ ^ 2 * ↑d + ↑s ^ 2 * ↑↑ℏ ^ 2) • 𝐫₀ ε (-2 + s) -
    (-(↑s * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s) I_sq,d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) -
      (↑s * -1 * ↑↑ℏ ^ 2 * ↑d + (-(↑s * -1 * ↑↑ℏ ^ 2 * 2) + ↑s ^ 2 * -1 * ↑↑ℏ ^ 2)) • 𝐫₀ ε (-2 + s) +
    (-(↑s * -1 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * -1 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s) =
  (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) +
      (-(↑s * ↑↑ℏ ^ 2 * 2) + ↑s * ↑↑ℏ ^ 2 * ↑d + ↑s ^ 2 * ↑↑ℏ ^ 2) • 𝐫₀ ε (-2 + s) -
    (-(↑s * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s) sub_eq_add_neg,d:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) +
      -((↑s * -1 * ↑↑ℏ ^ 2 * ↑d + (-(↑s * -1 * ↑↑ℏ ^ 2 * 2) + ↑s ^ 2 * -1 * ↑↑ℏ ^ 2)) • 𝐫₀ ε (-2 + s)) +
    (-(↑s * -1 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * -1 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s) =
  (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) +
      (-(↑s * ↑↑ℏ ^ 2 * 2) + ↑s * ↑↑ℏ ^ 2 * ↑d + ↑s ^ 2 * ↑↑ℏ ^ 2) • 𝐫₀ ε (-2 + s) +
    -((-(↑s * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s)) ← neg_smuld:ℕε:ℝˣs:ℝ⊢ (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) +
      -(↑s * -1 * ↑↑ℏ ^ 2 * ↑d + (-(↑s * -1 * ↑↑ℏ ^ 2 * 2) + ↑s ^ 2 * -1 * ↑↑ℏ ^ 2)) • 𝐫₀ ε (-2 + s) +
    (-(↑s * -1 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * -1 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s) =
  (↑s * I * ↑↑ℏ * 2) • 𝐫₀ ε (-2 + s) ∘SL (𝐱 ⬝ᵥ 𝐩) +
      (-(↑s * ↑↑ℏ ^ 2 * 2) + ↑s * ↑↑ℏ ^ 2 * ↑d + ↑s ^ 2 * ↑↑ℏ ^ 2) • 𝐫₀ ε (-2 + s) +
    -(-(↑s * ↑↑ℏ ^ 2 * ↑↑ε ^ 2 * 2) + ↑s ^ 2 * ↑↑ℏ ^ 2 * ↑↑ε ^ 2) • 𝐫₀ ε (-4 + s)]
      ring_nfAll goals completed! 🐙

B.4. Angular momentum / position

              lemma angularMomentum_commutation_position :
    ⁅𝐋 i j, 𝐱 k⁆ = (I * ℏ) • (δ[i,k] • 𝐱 j - δ[j,k] • 𝐱 i) := byd:ℕi:Fin dj:Fin dk:Fin d⊢ ⁅𝐋 i j, 𝐱 k⁆ = (I * ↑↑ℏ) • (δ[i,k] • 𝐱 j - δ[j,k] • 𝐱 i)
  trans 𝐱 i ∘L ⁅𝐩 j, 𝐱 k⁆ - 𝐱 j ∘L ⁅𝐩 i, 𝐱 k⁆d:ℕi:Fin dj:Fin dk:Fin d⊢ ⁅𝐋 i j, 𝐱 k⁆ = 𝐱 i ∘SL ⁅𝐩 j, 𝐱 k⁆ - 𝐱 j ∘SL ⁅𝐩 i, 𝐱 k⁆d:ℕi:Fin dj:Fin dk:Fin d⊢ 𝐱 i ∘SL ⁅𝐩 j, 𝐱 k⁆ - 𝐱 j ∘SL ⁅𝐩 i, 𝐱 k⁆ = (I * ↑↑ℏ) • (δ[i,k] • 𝐱 j - δ[j,k] • 𝐱 i)
  ·d:ℕi:Fin dj:Fin dk:Fin d⊢ ⁅𝐋 i j, 𝐱 k⁆ = 𝐱 i ∘SL ⁅𝐩 j, 𝐱 k⁆ - 𝐱 j ∘SL ⁅𝐩 i, 𝐱 k⁆ simp [angularMomentumOperator, leibniz_lie]All goals completed! 🐙
  simp only [← lie_skew (𝐩 _), comp_neg, sub_neg_eq_add, add_comm, ← sub_eq_add_neg,
    position_commutation_momentum, comp_smul, comp_id, smul_sub, symm k _]All goals completed! 🐙@[simp]
lemma angularMomentum_commutation_radiusRegPow : ⁅𝐋 i j, 𝐫₀[d] ε s⁆ = 0 := byd:ℕi:Fin dj:Fin dε:ℝˣs:ℝ⊢ ⁅𝐋 i j, 𝐫₀ ε s⁆ = 0
  trans 𝐱 i ∘L ⁅𝐩 j, 𝐫₀ ε s⁆ - 𝐱 j ∘L ⁅𝐩 i, 𝐫₀ ε s⁆d:ℕi:Fin dj:Fin dε:ℝˣs:ℝ⊢ ⁅𝐋 i j, 𝐫₀ ε s⁆ = 𝐱 i ∘SL ⁅𝐩 j, 𝐫₀ ε s⁆ - 𝐱 j ∘SL ⁅𝐩 i, 𝐫₀ ε s⁆d:ℕi:Fin dj:Fin dε:ℝˣs:ℝ⊢ 𝐱 i ∘SL ⁅𝐩 j, 𝐫₀ ε s⁆ - 𝐱 j ∘SL ⁅𝐩 i, 𝐫₀ ε s⁆ = 0
  ·d:ℕi:Fin dj:Fin dε:ℝˣs:ℝ⊢ ⁅𝐋 i j, 𝐫₀ ε s⁆ = 𝐱 i ∘SL ⁅𝐩 j, 𝐫₀ ε s⁆ - 𝐱 j ∘SL ⁅𝐩 i, 𝐫₀ ε s⁆ simp [angularMomentumOperator, leibniz_lie]All goals completed! 🐙
  simp [← lie_skew (𝐩 _), radiusRegPow_commutation_momentum, comp_neg,
    ← position_comp_radiusRegPow_commute, ← comp_assoc, position_comp_commute]All goals completed! 🐙

lemma angularMomentum_comp_radiusRegPow_commute : 𝐋 i j ∘L 𝐫₀ ε s = 𝐫₀ ε s ∘L 𝐋 i j := byd:ℕi:Fin dj:Fin dε:ℝˣs:ℝ⊢ 𝐋 i j ∘SL 𝐫₀ ε s = 𝐫₀ ε s ∘SL 𝐋 i j
  rw [comp_eq_comp_add_commute,d:ℕi:Fin dj:Fin dε:ℝˣs:ℝ⊢ 𝐫₀ ε s ∘SL 𝐋 i j + ⁅𝐋 i j, 𝐫₀ ε s⁆ = 𝐫₀ ε s ∘SL 𝐋 i jAll goals completed! 🐙 angularMomentum_commutation_radiusRegPow,d:ℕi:Fin dj:Fin dε:ℝˣs:ℝ⊢ 𝐫₀ ε s ∘SL 𝐋 i j + 0 = 𝐫₀ ε s ∘SL 𝐋 i jAll goals completed! 🐙 add_zerod:ℕi:Fin dj:Fin dε:ℝˣs:ℝ⊢ 𝐫₀ ε s ∘SL 𝐋 i j = 𝐫₀ ε s ∘SL 𝐋 i jAll goals completed! 🐙]All goals completed! 🐙@[simp]
lemma angularMomentumSqr_commutation_radiusRegPow : ⁅𝐋²[d], 𝐫₀[d] ε s⁆ = 0 := byd:ℕε:ℝˣs:ℝ⊢ ⁅𝐋², 𝐫₀ ε s⁆ = 0
  simp [angularMomentumOperatorSqr, sum_lie, leibniz_lie]All goals completed! 🐙

lemma angularMomentumSqr_comp_radiusRegPow_commute : 𝐋² ∘L 𝐫₀[d] ε s = 𝐫₀ ε s ∘L 𝐋² := byd:ℕε:ℝˣs:ℝ⊢ 𝐋² ∘SL 𝐫₀ ε s = 𝐫₀ ε s ∘SL 𝐋²
  rw [comp_eq_comp_add_commute,d:ℕε:ℝˣs:ℝ⊢ 𝐫₀ ε s ∘SL 𝐋² + ⁅𝐋², 𝐫₀ ε s⁆ = 𝐫₀ ε s ∘SL 𝐋²All goals completed! 🐙 angularMomentumSqr_commutation_radiusRegPow,d:ℕε:ℝˣs:ℝ⊢ 𝐫₀ ε s ∘SL 𝐋² + 0 = 𝐫₀ ε s ∘SL 𝐋²All goals completed! 🐙 add_zerod:ℕε:ℝˣs:ℝ⊢ 𝐫₀ ε s ∘SL 𝐋² = 𝐫₀ ε s ∘SL 𝐋²All goals completed! 🐙]All goals completed! 🐙

B.5. Angular momentum / momentum

              lemma angularMomentum_commutation_momentum :
    ⁅𝐋 i j, 𝐩 k⁆ = (I * ℏ) • (δ[i,k] • 𝐩 j - δ[j,k] • 𝐩 i) := byd:ℕi:Fin dj:Fin dk:Fin d⊢ ⁅𝐋 i j, 𝐩 k⁆ = (I * ↑↑ℏ) • (δ[i,k] • 𝐩 j - δ[j,k] • 𝐩 i)
  trans ⁅𝐱 i, 𝐩 k⁆ ∘L 𝐩 j - ⁅𝐱 j, 𝐩 k⁆ ∘L 𝐩 id:ℕi:Fin dj:Fin dk:Fin d⊢ ⁅𝐋 i j, 𝐩 k⁆ = ⁅𝐱 i, 𝐩 k⁆ ∘SL 𝐩 j - ⁅𝐱 j, 𝐩 k⁆ ∘SL 𝐩 id:ℕi:Fin dj:Fin dk:Fin d⊢ ⁅𝐱 i, 𝐩 k⁆ ∘SL 𝐩 j - ⁅𝐱 j, 𝐩 k⁆ ∘SL 𝐩 i = (I * ↑↑ℏ) • (δ[i,k] • 𝐩 j - δ[j,k] • 𝐩 i)
  ·d:ℕi:Fin dj:Fin dk:Fin d⊢ ⁅𝐋 i j, 𝐩 k⁆ = ⁅𝐱 i, 𝐩 k⁆ ∘SL 𝐩 j - ⁅𝐱 j, 𝐩 k⁆ ∘SL 𝐩 i simp [angularMomentumOperator, leibniz_lie]All goals completed! 🐙
  simp only [position_commutation_momentum, smul_comp, id_comp, smul_sub]All goals completed! 🐙

lemma momentum_comp_angularMomentum_eq :
    𝐩 k ∘L 𝐋 i j = 𝐋 i j ∘L 𝐩 k - (I * ℏ) • (δ[i,k] • 𝐩 j - δ[j,k] • 𝐩 i) := byd:ℕi:Fin dj:Fin dk:Fin d⊢ 𝐩 k ∘SL 𝐋 i j = 𝐋 i j ∘SL 𝐩 k - (I * ↑↑ℏ) • (δ[i,k] • 𝐩 j - δ[j,k] • 𝐩 i)
  rw [comp_eq_comp_sub_commute,d:ℕi:Fin dj:Fin dk:Fin d⊢ 𝐋 i j ∘SL 𝐩 k - ⁅𝐋 i j, 𝐩 k⁆ = 𝐋 i j ∘SL 𝐩 k - (I * ↑↑ℏ) • (δ[i,k] • 𝐩 j - δ[j,k] • 𝐩 i)All goals completed! 🐙 angularMomentum_commutation_momentumd:ℕi:Fin dj:Fin dk:Fin d⊢ 𝐋 i j ∘SL 𝐩 k - (I * ↑↑ℏ) • (δ[i,k] • 𝐩 j - δ[j,k] • 𝐩 i) = 𝐋 i j ∘SL 𝐩 k - (I * ↑↑ℏ) • (δ[i,k] • 𝐩 j - δ[j,k] • 𝐩 i)All goals completed! 🐙]All goals completed! 🐙@[simp]
lemma angularMomentum_commutation_momentumSqr : ⁅𝐋 i j, 𝐩[d] ⬝ᵥ 𝐩⁆ = 0 := byd:ℕi:Fin dj:Fin d⊢ ⁅𝐋 i j, 𝐩 ⬝ᵥ 𝐩⁆ = 0
  simp only [dotProduct, mul_def, lie_sum, lie_leibniz, angularMomentum_commutation_momentum,
    comp_smul, comp_sub, smul_comp, sub_comp, ← smul_add, ← Finset.smul_sum, Finset.sum_add_distrib,
    Finset.sum_sub_distrib, sum_smul, sub_add_sub_cancel, sub_self, smul_zero]All goals completed! 🐙

lemma momentumSqr_comp_angularMomentum_commute : (𝐩 ⬝ᵥ 𝐩) ∘L 𝐋 i j = 𝐋 i j ∘L (𝐩 ⬝ᵥ 𝐩) := byd:ℕi:Fin dj:Fin d⊢ (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j = 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩)
  rw [comp_eq_comp_sub_commute,d:ℕi:Fin dj:Fin d⊢ 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩) - ⁅𝐋 i j, 𝐩 ⬝ᵥ 𝐩⁆ = 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩)All goals completed! 🐙 angularMomentum_commutation_momentumSqr,d:ℕi:Fin dj:Fin d⊢ 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩) - 0 = 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩)All goals completed! 🐙 sub_zerod:ℕi:Fin dj:Fin d⊢ 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩) = 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩)All goals completed! 🐙]All goals completed! 🐙@[simp]
lemma angularMomentumSqr_commutation_momentumSqr : ⁅𝐋²[d], 𝐩[d] ⬝ᵥ 𝐩⁆ = 0 := byd:ℕ⊢ ⁅𝐋², 𝐩 ⬝ᵥ 𝐩⁆ = 0
  simp [angularMomentumOperatorSqr, sum_lie, leibniz_lie]All goals completed! 🐙

B.6. Angular momentum / angular momentum

lemma angularMomentum_commutation_angularMomentum : ⁅𝐋 i j, 𝐋 k l⁆ =
    (I * ℏ) • (δ[i,k] • 𝐋 j l - δ[i,l] • 𝐋 j k - δ[j,k] • 𝐋 i l + δ[j,l] • 𝐋 i k) := byd:ℕi:Fin dj:Fin dk:Fin dl:Fin d⊢ ⁅𝐋 i j, 𝐋 k l⁆ = (I * ↑↑ℏ) • (δ[i,k] • 𝐋 j l - δ[i,l] • 𝐋 j k - δ[j,k] • 𝐋 i l + δ[j,l] • 𝐋 i k)
  nth_rw 2 [angularMomentumOperatord:ℕi:Fin dj:Fin dk:Fin dl:Fin d⊢ ⁅𝐋 i j, 𝐱 k ∘SL 𝐩 l - 𝐱 l ∘SL 𝐩 k⁆ = (I * ↑↑ℏ) • (δ[i,k] • 𝐋 j l - δ[i,l] • 𝐋 j k - δ[j,k] • 𝐋 i l + δ[j,l] • 𝐋 i k)]d:ℕi:Fin dj:Fin dk:Fin dl:Fin d⊢ ⁅𝐋 i j, 𝐱 k ∘SL 𝐩 l - 𝐱 l ∘SL 𝐩 k⁆ = (I * ↑↑ℏ) • (δ[i,k] • 𝐋 j l - δ[i,l] • 𝐋 j k - δ[j,k] • 𝐋 i l + δ[j,l] • 𝐋 i k)
  simp only [angularMomentum_commutation_position, angularMomentum_commutation_momentum,
    lie_sub, lie_leibniz, comp_smul, smul_comp, comp_sub, sub_comp, ← smul_add, ← smul_sub]d:ℕi:Fin dj:Fin dk:Fin dl:Fin d⊢ (I * ↑↑ℏ) •
    (δ[i,l] • 𝐱 k ∘SL 𝐩 j - δ[j,l] • 𝐱 k ∘SL 𝐩 i + (δ[i,k] • 𝐱 j ∘SL 𝐩 l - δ[j,k] • 𝐱 i ∘SL 𝐩 l) -
      (δ[i,k] • 𝐱 l ∘SL 𝐩 j - δ[j,k] • 𝐱 l ∘SL 𝐩 i + (δ[i,l] • 𝐱 j ∘SL 𝐩 k - δ[j,l] • 𝐱 i ∘SL 𝐩 k))) =
  (I * ↑↑ℏ) • (δ[i,k] • 𝐋 j l - δ[i,l] • 𝐋 j k - δ[j,k] • 𝐋 i l + δ[j,l] • 𝐋 i k)
  dsimp [angularMomentumOperator]d:ℕi:Fin dj:Fin dk:Fin dl:Fin d⊢ (I * ↑↑ℏ) •
    (δ[i,l] • 𝐱 k ∘SL 𝐩 j - δ[j,l] • 𝐱 k ∘SL 𝐩 i + (δ[i,k] • 𝐱 j ∘SL 𝐩 l - δ[j,k] • 𝐱 i ∘SL 𝐩 l) -
      (δ[i,k] • 𝐱 l ∘SL 𝐩 j - δ[j,k] • 𝐱 l ∘SL 𝐩 i + (δ[i,l] • 𝐱 j ∘SL 𝐩 k - δ[j,l] • 𝐱 i ∘SL 𝐩 k))) =
  (I * ↑↑ℏ) •
    (δ[i,k] • (𝐱 j ∘SL 𝐩 l - 𝐱 l ∘SL 𝐩 j) - δ[i,l] • (𝐱 j ∘SL 𝐩 k - 𝐱 k ∘SL 𝐩 j) -
        δ[j,k] • (𝐱 i ∘SL 𝐩 l - 𝐱 l ∘SL 𝐩 i) +
      δ[j,l] • (𝐱 i ∘SL 𝐩 k - 𝐱 k ∘SL 𝐩 i))
  extd:ℕi:Fin dj:Fin dk:Fin dl:Fin dx✝¹:𝓢(Space d, ℂ)x✝:Space d⊢ (((I * ↑↑ℏ) •
        (δ[i,l] • 𝐱 k ∘SL 𝐩 j - δ[j,l] • 𝐱 k ∘SL 𝐩 i + (δ[i,k] • 𝐱 j ∘SL 𝐩 l - δ[j,k] • 𝐱 i ∘SL 𝐩 l) -
          (δ[i,k] • 𝐱 l ∘SL 𝐩 j - δ[j,k] • 𝐱 l ∘SL 𝐩 i + (δ[i,l] • 𝐱 j ∘SL 𝐩 k - δ[j,l] • 𝐱 i ∘SL 𝐩 k))))
      x✝¹)
    x✝ =
  (((I * ↑↑ℏ) •
        (δ[i,k] • (𝐱 j ∘SL 𝐩 l - 𝐱 l ∘SL 𝐩 j) - δ[i,l] • (𝐱 j ∘SL 𝐩 k - 𝐱 k ∘SL 𝐩 j) -
            δ[j,k] • (𝐱 i ∘SL 𝐩 l - 𝐱 l ∘SL 𝐩 i) +
          δ[j,l] • (𝐱 i ∘SL 𝐩 k - 𝐱 k ∘SL 𝐩 i)))
      x✝¹)
    x✝
  simp only [nsmul_eq_mul, smul_apply, sub_apply, add_apply, mul_apply_eq_comp, comp_apply,
    _root_.natCast_apply, positionCLM_apply, momentumCLM_apply, neg_mul, mul_neg, smul_neg,
    sub_neg_eq_add, smul_eq_mul, smul_add]d:ℕi:Fin dj:Fin dk:Fin dl:Fin dx✝¹:𝓢(Space d, ℂ)x✝:Space d⊢ I * ↑↑ℏ *
    (-(↑δ[i,l] * (↑(x✝.val k) * (I * ↑↑ℏ * Space.deriv j (⇑x✝¹) x✝))) +
          ↑δ[j,l] * (↑(x✝.val k) * (I * ↑↑ℏ * Space.deriv i (⇑x✝¹) x✝)) +
        (-(↑δ[i,k] * (↑(x✝.val j) * (I * ↑↑ℏ * Space.deriv l (⇑x✝¹) x✝))) +
          ↑δ[j,k] * (↑(x✝.val i) * (I * ↑↑ℏ * Space.deriv l (⇑x✝¹) x✝))) -
      (-(↑δ[i,k] * (↑(x✝.val l) * (I * ↑↑ℏ * Space.deriv j (⇑x✝¹) x✝))) +
          ↑δ[j,k] * (↑(x✝.val l) * (I * ↑↑ℏ * Space.deriv i (⇑x✝¹) x✝)) +
        (-(↑δ[i,l] * (↑(x✝.val j) * (I * ↑↑ℏ * Space.deriv k (⇑x✝¹) x✝))) +
          ↑δ[j,l] * (↑(x✝.val i) * (I * ↑↑ℏ * Space.deriv k (⇑x✝¹) x✝))))) =
  I * ↑↑ℏ *
      (-(↑δ[i,k] * (↑(x✝.val j) * (I * ↑↑ℏ * Space.deriv l (⇑x✝¹) x✝))) +
            ↑δ[i,k] * (↑(x✝.val l) * (I * ↑↑ℏ * Space.deriv j (⇑x✝¹) x✝)) -
          (-(↑δ[i,l] * (↑(x✝.val j) * (I * ↑↑ℏ * Space.deriv k (⇑x✝¹) x✝))) +
            ↑δ[i,l] * (↑(x✝.val k) * (I * ↑↑ℏ * Space.deriv j (⇑x✝¹) x✝))) -
        (-(↑δ[j,k] * (↑(x✝.val i) * (I * ↑↑ℏ * Space.deriv l (⇑x✝¹) x✝))) +
          ↑δ[j,k] * (↑(x✝.val l) * (I * ↑↑ℏ * Space.deriv i (⇑x✝¹) x✝)))) +
    I * ↑↑ℏ *
      (-(↑δ[j,l] * (↑(x✝.val i) * (I * ↑↑ℏ * Space.deriv k (⇑x✝¹) x✝))) +
        ↑δ[j,l] * (↑(x✝.val k) * (I * ↑↑ℏ * Space.deriv i (⇑x✝¹) x✝)))
  ringAll goals completed! 🐙

@[simp]
lemma angularMomentumSqr_commutation_angularMomentum : ⁅𝐋²[d], 𝐋 i j⁆ = 0 := byd:ℕi:Fin dj:Fin d⊢ ⁅𝐋², 𝐋 i j⁆ = 0
  simp only [angularMomentumOperatorSqr, smul_lie, sum_lie, leibniz_lie, ← smul_add, comp_smul,
    comp_add, comp_sub, smul_comp, add_comp, sub_comp, angularMomentum_commutation_angularMomentum,
    angularMomentumOperator_antisymm _ i, angularMomentumOperator_antisymm j _, symm _ i, symm _ j,
    sum_smul, ← Finset.smul_sum, Finset.sum_add_distrib, Finset.sum_sub_distrib]d:ℕi:Fin dj:Fin d⊢ 2⁻¹ •
    (I * ↑↑ℏ) •
      (∑ x, 𝐋 i x ∘SL 𝐋 x j - ∑ x, (-𝐋 x j) ∘SL (-𝐋 i x) - ∑ x, (-𝐋 i x) ∘SL 𝐋 x j + ∑ x, 𝐋 x j ∘SL (-𝐋 i x) +
        (∑ x, 𝐋 x j ∘SL 𝐋 i x - ∑ x, (-𝐋 i x) ∘SL (-𝐋 x j) - ∑ x, 𝐋 x j ∘SL (-𝐋 i x) + ∑ x, (-𝐋 i x) ∘SL 𝐋 x j)) =
  0
  abel_nfd:ℕi:Fin dj:Fin d⊢ 2⁻¹ •
    (I * ↑↑ℏ) •
      (∑ x, 𝐋 i x ∘SL 𝐋 x j +
        (-1 • ∑ x, (-1 • 𝐋 x j) ∘SL (-1 • 𝐋 i x) + (∑ x, 𝐋 x j ∘SL 𝐋 i x + -1 • ∑ x, (-1 • 𝐋 i x) ∘SL (-1 • 𝐋 x j)))) =
  0
  simp [smul_zero]All goals completed! 🐙