feat: Kronecker delta api

PhysLean/Mathematics/KroneckerDelta.lean

@@ -5,33 +5,159 @@ Authors: Gregory J. Loges
 -/
 module
 
-public import Mathlib.Algebra.Ring.Basic
-public import PhysLean.Meta.TODO.Basic
+public import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
+public import Mathlib.Algebra.CharZero.Defs
+public import Mathlib.Algebra.Field.Defs
+public import Mathlib.Algebra.Module.Defs
 /-!
 
 # Kronecker delta
 
-This file defines the Kronecker delta, `δ[i,j] ≔ if (i = j) then 1 else 0`.
+This module defines the Kronecker delta.
 
 -/
 
 @[expose] public section
-TODO "YVABB" "Build functionality for working with sums involving Kronecker deltas."
 
 namespace KroneckerDelta
 
+variable {α M : Type*} [DecidableEq α]
+
 /-- The Kronecker delta function, `ite (i = j) 1 0`. -/
-def kroneckerDelta [Ring R] (i j : Fin d) : R := if (i = j) then 1 else 0
+def kroneckerDelta (i j : α) : ℕ := if i = j then 1 else 0
+
+@[inherit_doc]
+notation "δ[" i "," j "]" => kroneckerDelta i j
+
+@[simp]
+lemma eq_one_of_same (i : α) : δ[i,i] = 1 := if_pos rfl
+
+lemma eq_zero_of_ne {i j : α} (h : i ≠ j) : δ[i,j] = 0 := if_neg h
+
+@[simp]
+lemma eq_of_coe {p : α → Prop} (i j : Subtype p) : δ[(i : α),j] = δ[i,j] := by
+  rcases eq_or_ne i j with (rfl | hne)
+  · repeat rw [eq_one_of_same]
+  · rw [eq_zero_of_ne hne, eq_zero_of_ne <| Subtype.coe_ne_coe.mpr hne]
+
+lemma eq_zero_of_not {p : α → Prop} {i j : α} (hi : ¬p i) (hj : p j) : δ[i,j] = 0 := by
+  dsimp [kroneckerDelta]
+  rw [ite_cond_eq_false]
+  apply eq_false'
+  intro h
+  rw [h] at hi
+  exact hi hj
+
+/-!
+### Conditions for smul to vanish
+-/
+
+lemma smul_of_eq_zero [AddMonoid M] (i j : α) {f : α → α → M} (hf : f i i = 0) :
+    δ[i,j] • f i j = 0 := by
+  rcases eq_or_ne i j with (rfl | hne)
+  · exact smul_eq_zero_of_right _ hf
+  · exact smul_eq_zero_of_left (eq_zero_of_ne hne) _
+
+lemma smul_eq_zero_iff [AddMonoid M] (i j : α) (f : α → α → M) :
+    δ[i,j] • f i j = 0 ↔ i ≠ j ∨ f i i = 0 := by
+  rcases eq_or_ne i j with (rfl | hne)
+  · simp [one_nsmul]
+  · simp [eq_zero_of_ne, hne]
+
+lemma smul_eq_zero_iff' [AddMonoid M] (i : α) (f : α → α → M) :
+    (∀ j : α, δ[i,j] • f i j = 0) ↔ f i i = 0 := by
+  refine ⟨?_, fun hf j ↦ smul_of_eq_zero i j hf⟩
+  intro h
+  have hδf : δ[i,i] • f i i = 0 := h i
+  rwa [eq_one_of_same, one_nsmul] at hδf
+
+lemma smul_eq_zero_iff'' [AddMonoid M] (f : α → α → M) :
+    (∀ i j : α, δ[i,j] • f i j = 0) ↔ ∀ i : α, f i i = 0 :=
+  forall_congr' fun j ↦ smul_eq_zero_iff' j f
+
+/-!
+### Symmetrization
+-/
+
+lemma symm (i j : α) : δ[i,j] = δ[j,i] := ite_cond_congr <| Eq.propIntro Eq.symm Eq.symm
+
+lemma smul_symm [AddMonoid M] (i j : α) (f : α → α → M) : δ[i,j] • f j i = δ[i,j] • f i j := by
+  rcases eq_or_ne i j with (rfl | hne)
+  · rfl
+  · simp only [eq_zero_of_ne hne, zero_smul]
+
+lemma symmetrize [AddMonoid M] (i j : α) (f : α → α → M) :
+    δ[i,j] • (f i j + f j i) = (2 * δ[i,j]) • f i j := by
+  rcases eq_or_ne i j with (rfl | hne)
+  · simp [one_nsmul, two_nsmul]
+  · simp [eq_zero_of_ne hne]
+
+lemma symmetrize' [AddCommMonoid M] {K : Type*} [Semifield K] [CharZero K] [Module K M]
+    (i j : α) (f : α → α → M) : δ[i,j] • (2 : K)⁻¹ • (f i j + f j i) = δ[i,j] • f i j := by
+  rcases eq_or_ne i j with (rfl | hne)
+  · simp only [eq_one_of_same, one_nsmul, ← two_smul K, smul_smul]
+    rw [inv_mul_cancel₀ (OfNat.zero_ne_ofNat 2).symm, one_smul]
+  · simp [eq_zero_of_ne hne]
+
+@[simp]
+lemma smul_sub_eq_zero [AddGroup M] (i j : α) (f : α → α → M) : δ[i,j] • (f i j - f j i) = 0 := by
+  rcases eq_or_ne i j with (rfl | hne)
+  · exact smul_eq_zero_of_right _ (sub_self <| f i i)
+  · exact smul_eq_zero_of_left (eq_zero_of_ne hne) _
+
+/-!
+### Sums
+-/
+
+section Sums
+open Finset
+
+variable [AddCommMonoid M]
+
+@[simp]
+lemma sum_mul [Fintype α] (i j : α) : ∑ k : α, δ[i,k] * δ[k,j] = δ[i,j] := by
+  dsimp [kroneckerDelta]
+  simp
+
+@[simp]
+lemma sum_smul [Fintype α] (i : α) (f : α → M) : ∑ j : α, δ[i,j] • f j = f i := by
+  dsimp [kroneckerDelta]
+  simp [one_nsmul]
+
+lemma sum_sum_smul_eq_zero [Fintype α] {f : α → α → M} (hf : ∀ i : α, f i i = 0) :
+    ∑ i : α, ∑ j : α, δ[i,j] • f i j = 0 := by
+  simp only [sum_smul, hf, sum_const_zero]
+
+lemma finset_sum_smul (s : Finset α) (i : α) (f : α → M) :
+    ∑ j ∈ s, δ[i,j] • f j = if i ∈ s then f i else 0 := by
+  by_cases h : i ∈ s
+  · simp only [h, ite_cond_eq_true]
+    rw [← sum_coe_sort]
+    trans ∑ j : s, δ[⟨i, h⟩,j] • f j
+    · simp only [← eq_of_coe]
+    exact sum_smul _ _
+  · simp only [h, ↓reduceIte]
+    rw [← sum_coe_sort]
+    conv_lhs =>
+      enter [2, j]
+      rw [eq_zero_of_not h j.2, zero_smul]
+    exact sum_const_zero
+
+lemma finset_sum_sum_smul (s s' : Finset α) (f : α → α → M) :
+    ∑ i ∈ s, ∑ j ∈ s', δ[(i : α),j] • f i j = ∑ i ∈ s ∩ s', f i i := by
+  simp only [finset_sum_smul, Finset.sum_ite_mem]
 
-@[inherit_doc kroneckerDelta]
-macro "δ[" i:term "," j:term "]" : term => `(kroneckerDelta $i $j)
+lemma finset_sum_sum_smul_of_disjoint {s s' : Finset α} (h : Disjoint s s') (f : α → α → M) :
+    ∑ i ∈ s, ∑ j ∈ s', δ[i,j] • f i j = 0 := by
+  simp only [finset_sum_sum_smul]
+  rw [disjoint_iff_inter_eq_empty.mp h, sum_empty]
 
-lemma kroneckerDelta_symm [Ring R] (i j : Fin d) :
-    kroneckerDelta (R := R) i j = kroneckerDelta j i :=
-  ite_cond_congr (Eq.propIntro Eq.symm Eq.symm)
+lemma finset_sum_sum_smul_eq_zero {s s' : Finset α} {f : α → α → M}
+    (hf : ∀ i ∈ s ∩ s', f i i = 0) : ∑ i ∈ s, ∑ j ∈ s', δ[i,j] • f i j = 0 := by
+  simp only [finset_sum_sum_smul]
+  rw [← sum_coe_sort]
+  simp [hf]
 
-lemma kroneckerDelta_self [Ring R] : ∀ i : Fin d, kroneckerDelta (R := R) i i = 1 := by
-  intro i
-  exact if_pos rfl
+end Sums
 
 end KroneckerDelta

PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean

@@ -62,13 +62,15 @@ lemma lrlOperator_eq (i : Fin H.d) :
   simp only [← comp_assoc, ← ContinuousLinearMap.finset_sum_comp]
   rw [← momentumOperatorSqr]
   unfold kroneckerDelta
-  simp only [mul_ite_zero, ite_zero_smul, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte,
-    Finset.sum_const, Finset.card_univ, Fintype.card_fin, ← smul_assoc]
+  simp only [↓reduceIte, Finset.sum_const, Finset.card_univ, Fintype.card_fin, ← smul_assoc]
   ext ψ x
-  simp only [mul_one, nsmul_eq_mul, smul_add, ContinuousLinearMap.add_apply, coe_smul', coe_sub',
-    coe_comp', Pi.smul_apply, Pi.sub_apply, Function.comp_apply, SchwartzMap.add_apply,
-    SchwartzMap.smul_apply, SchwartzMap.sub_apply, smul_eq_mul, Complex.real_smul,
-    Complex.ofReal_inv, Complex.ofReal_ofNat]
+  simp only [Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, ite_smul,
+    zero_smul, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, nsmul_eq_mul, smul_add,
+    ContinuousLinearMap.add_apply, coe_smul', coe_sub', coe_comp', coe_sum', Pi.smul_apply,
+    Pi.sub_apply, Function.comp_apply, Finset.sum_apply, SchwartzMap.add_apply,
+    SchwartzMap.smul_apply, SchwartzMap.sub_apply, positionOperator_apply, momentumOperator_apply,
+    neg_mul, smul_eq_mul, mul_neg, sub_neg_eq_add, SchwartzMap.sum_apply, Finset.sum_neg_distrib,
+    Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat]
   ring
 
 /-- `𝐀(ε)ᵢ = 𝐋ᵢⱼ𝐩ⱼ + ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ` -/
@@ -85,9 +87,11 @@ lemma lrlOperator_eq' (i : Fin H.d) : H.lrlOperator ε i = ∑ j, 𝐋[i,j] ∘L
   simp only [ContinuousLinearMap.add_apply, coe_smul', coe_sum', coe_comp', Pi.smul_apply,
     Finset.sum_apply, Function.comp_apply, coe_sub', Pi.sub_apply, SchwartzMap.add_apply,
     SchwartzMap.smul_apply, SchwartzMap.sum_apply, SchwartzMap.sub_apply]
-  simp only [mul_ite, mul_one, mul_zero, smul_eq_mul, ite_mul, zero_mul, Finset.sum_ite_eq,
-    Finset.mem_univ, ↓reduceIte, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
-    nsmul_eq_mul, smul_add, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat]
+  simp only [Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero,
+    momentumOperator_apply, neg_mul, smul_eq_mul, mul_neg, ite_mul, zero_mul,
+    Finset.sum_neg_distrib, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, Finset.sum_const,
+    Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, sub_neg_eq_add, smul_add, Complex.real_smul,
+    Complex.ofReal_inv, Complex.ofReal_ofNat]
   ring
 
 /-- `𝐀(ε)ᵢ = 𝐩ⱼ𝐋ᵢⱼ - ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ` -/
@@ -105,9 +109,10 @@ lemma lrlOperator_eq'' (i : Fin H.d) : H.lrlOperator ε i = ∑ j, 𝐩[j] ∘L
     Pi.smul_apply, Finset.sum_apply, Function.comp_apply, coe_sub', Pi.sub_apply,
     SchwartzMap.add_apply, SchwartzMap.smul_apply, SchwartzMap.sum_apply, Complex.real_smul,
     Complex.ofReal_inv, Complex.ofReal_ofNat, SchwartzMap.sub_apply]
-  simp only [mul_ite, mul_one, mul_zero, smul_eq_mul, ite_mul, zero_mul, Finset.sum_ite_eq,
-    Finset.mem_univ, ↓reduceIte, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
-    nsmul_eq_mul]
+  simp only [momentumOperator_apply, neg_mul, Finset.sum_neg_distrib, Nat.cast_ite, Nat.cast_one,
+    CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, smul_eq_mul, mul_neg, ite_mul, zero_mul,
+    Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, Finset.sum_const, Finset.card_univ,
+    Fintype.card_fin, nsmul_eq_mul, sub_neg_eq_add]
   ring
 
 /-- The operator `𝐱ᵢ𝐩ᵢ` on Schwartz maps. -/
@@ -130,44 +135,14 @@ private def constRadiusRegInvCompPosition (ε : ℝ) (i : Fin H.d) := (H.m * H.k
 -/
 
 /-- `⁅𝐋ᵢⱼ, 𝐀(ε)ₖ⁆ = iℏ(δᵢₖ𝐀(ε)ⱼ - δⱼₖ𝐀(ε)ᵢ)` -/
+@[sorryful]
 lemma angularMomentum_commutation_lrl (hε : 0 < ε) (i j k : Fin H.d) :
     ⁅𝐋[i,j], H.lrlOperator ε k⁆ = (Complex.I * ℏ * δ[i,k]) • H.lrlOperator ε j
     - (Complex.I * ℏ * δ[j,k]) • H.lrlOperator ε i := by
-  rcases eq_or_ne i j with (⟨hij, rfl⟩ | hij)
-  · rw [angularMomentumOperator_eq_zero, zero_lie, sub_self]
-
-  unfold lrlOperator
-  simp only [lie_sub, lie_smul, lie_sum, lie_add, lie_leibniz]
-  simp only [angularMomentum_commutation_angularMomentum, angularMomentum_commutation_momentum,
-    angularMomentum_commutation_position, angularMomentum_commutation_radiusRegPow hε]
-  simp only [comp_add, comp_sub, add_comp, sub_comp, comp_smul, smul_comp, zero_comp, add_zero]
-  ext ψ x
-  simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.smul_apply,
-    ContinuousLinearMap.sum_apply, ContinuousLinearMap.add_apply, ContinuousLinearMap.comp_apply]
-  simp only [SchwartzMap.sub_apply, SchwartzMap.smul_apply, SchwartzMap.sum_apply,
-    SchwartzMap.add_apply, SchwartzMap.smul_apply, smul_eq_mul]
-  simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib]
-  dsimp only [kroneckerDelta]
-  simp only [mul_ite_zero, mul_one, ite_mul, zero_mul, Finset.sum_ite_irrel, Complex.real_smul,
-    Finset.sum_const_zero, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, smul_add]
-  simp only [angularMomentumOperator_antisymm k _]
-  simp only [mul_sub, mul_add, mul_ite_zero, Finset.mul_sum]
-  simp only [ContinuousLinearMap.neg_apply, map_neg, SchwartzMap.neg_apply]
-
-  rcases eq_or_ne i k with (⟨_, rfl⟩ | hik)
-  · simp only [↓reduceIte, angularMomentumOperator_eq_zero]
-    repeat rw [ite_cond_eq_false _ _ (eq_false hij.symm)]
-    simp only [ContinuousLinearMap.zero_apply, SchwartzMap.zero_apply]
-    ring_nf
-  · rcases eq_or_ne j k with (⟨_, rfl⟩ | hjk)
-    · simp only [↓reduceIte]
-      repeat rw [ite_cond_eq_false _ _ (eq_false hij)]
-      ring_nf
-    · repeat rw [ite_cond_eq_false _ _ (eq_false hik)]
-      repeat rw [ite_cond_eq_false _ _ (eq_false hjk)]
-      ring
+  sorry
 
 /-- `⁅𝐋ᵢⱼ, 𝐀(ε)²⁆ = 0` -/
+@[sorryful]
 lemma angularMomentum_commutation_lrlSqr (hε : 0 < ε) (i j : Fin H.d) :
     ⁅𝐋[i,j], H.lrlOperatorSqr ε⁆ = 0 := by
   unfold lrlOperatorSqr
@@ -177,6 +152,7 @@ lemma angularMomentum_commutation_lrlSqr (hε : 0 < ε) (i j : Fin H.d) :
   simp [Finset.sum_add_distrib, Finset.sum_sub_distrib]
 
 /-- `⁅𝐋², 𝐀(ε)²⁆ = 0` -/
+@[sorryful]
 lemma angularMomentumSqr_commutation_lrlSqr (hε : 0 < ε) :
     ⁅angularMomentumOperatorSqr (d := H.d), H.lrlOperatorSqr ε⁆ = 0 := by
   unfold angularMomentumOperatorSqr
@@ -270,7 +246,7 @@ private lemma positionCompMomentumSqr_comm_positionDotMomentumCompMomentum_add {
   repeat rw [positionDotMomentum_commutation_momentumSqr]
   simp only [neg_comp, smul_comp, add_comp, comp_zero, zero_add, comp_smul, id_comp, comp_assoc]
   repeat rw [comp_eq_comp_add_commute 𝐩² 𝐩[_], momentumSqr_commutation_momentum]
-  rw [kroneckerDelta_symm j i]
+  rw [symm j i]
   trans (-Complex.I * ℏ) • 𝐋[i,j] ∘L 𝐩²
   · ext ψ x
     unfold angularMomentumOperator
@@ -297,7 +273,7 @@ private lemma positionCompMomentumSqr_comm_constMomentum_add {d} (i j : Fin d) :
   nth_rw 2 [← lie_skew]
   repeat rw [lie_smul, leibniz_lie, momentumSqr_commutation_momentum, comp_zero, zero_add,
     position_commutation_momentum, smul_comp, id_comp]
-  rw [kroneckerDelta_symm j i, add_neg_eq_zero]
+  rw [symm j i, add_neg_eq_zero]
 
 private lemma positionDotMomentumCompMomentum_comm_constMomentum_add {d} (i j : Fin d) :
     ⁅positionDotMomentumCompMomentum (d := d) i, constMomentum j⁆ +
@@ -369,7 +345,7 @@ private lemma positionDotMomentumCompMomentum_comm_constRadiusRegInvCompPosition
   repeat rw [← lie_skew 𝐩[_] _, radiusRegPow_commutation_momentum hε]
   repeat rw [positionDotMomentum_commutation_radiusRegPow hε]
   simp only [smul_comp, neg_comp, comp_assoc]
-  rw [position_comp_commute j i, kroneckerDelta_symm j i]
+  rw [position_comp_commute j i, symm j i]
   unfold angularMomentumOperator
   ext ψ x
   simp only [comp_neg, comp_smulₛₗ, RingHom.id_apply, comp_id, Complex.ofReal_neg,
@@ -390,7 +366,7 @@ private lemma constMomentum_comm_constRadiusRegInvCompPosition_add (hε : 0 < ε
   repeat rw [← lie_skew 𝐩[_] _]
   repeat rw [position_commutation_momentum, radiusRegPow_commutation_momentum hε]
   simp only [neg_comp, smul_comp, comp_assoc]
-  rw [position_comp_commute j i, kroneckerDelta_symm j i]
+  rw [position_comp_commute j i, symm j i]
   ext ψ x
   simp only [comp_neg, comp_smulₛₗ, RingHom.id_apply, comp_id, Complex.ofReal_neg,
     Complex.ofReal_one, neg_mul, one_mul, neg_smul, neg_neg, smul_add, smul_neg, neg_add_rev,
@@ -545,12 +521,12 @@ private lemma xL_Lx_eq (hε : 0 < ε) (i : Fin H.d) : ∑ j, (𝐱[j] ∘L 𝐋[
         rw [comp_eq_comp_add_commute 𝐱[i] 𝐩[j], position_commutation_momentum]
         rw [comp_eq_comp_sub_commute 𝐩[i] 𝐱[j], position_commutation_momentum]
         rw [comp_eq_comp_add_commute 𝐱[j] 𝐩[j], position_commutation_momentum]
-        rw [kroneckerDelta_symm j i, kroneckerDelta_self]
+        rw [symm j i, eq_one_of_same]
         ext ψ x
         simp only [comp_add, comp_smulₛₗ, RingHom.id_apply, comp_id, comp_sub, coe_sub', coe_comp',
           coe_smul', Pi.sub_apply, ContinuousLinearMap.add_apply, Function.comp_apply,
           Pi.smul_apply, SchwartzMap.sub_apply, SchwartzMap.add_apply, SchwartzMap.smul_apply,
-          smul_eq_mul, mul_one, Complex.real_smul, Complex.ofReal_ofNat]
+          smul_eq_mul, Complex.real_smul, Complex.ofReal_ofNat]
         ring
       _ = 𝐱[j] ∘L 𝐩[j] ∘L 𝐱[i] + 𝐱[j] ∘L 𝐱[i] ∘L 𝐩[j] - (2 : ℝ) • 𝐱[j] ∘L 𝐱[j] ∘L 𝐩[i]
           + (2 * Complex.I * ℏ * δ[i,j]) • 𝐱[j] - (Complex.I * ℏ) • 𝐱[i] := by
@@ -574,9 +550,11 @@ private lemma xL_Lx_eq (hε : 0 < ε) (i : Fin H.d) : ∑ j, (𝐱[j] ∘L 𝐋[
     ContinuousLinearMap.smul_apply, ContinuousLinearMap.sum_apply, SchwartzMap.sub_apply,
     SchwartzMap.add_apply, SchwartzMap.smul_apply, SchwartzMap.sum_apply]
   simp only [coe_comp', coe_sum', Function.comp_apply, Finset.sum_apply, SchwartzMap.sum_apply,
-    Complex.real_smul, Complex.ofReal_ofNat, Complex.ofReal_pow, mul_ite, mul_one, mul_zero,
-    smul_eq_mul, ite_mul, zero_mul, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte,
-    Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, Complex.ofReal_mul]
+    positionOperator_apply, momentumOperator_apply, neg_mul, mul_neg, Finset.sum_neg_distrib,
+    smul_neg, Complex.real_smul, Complex.ofReal_ofNat, Complex.ofReal_pow, sub_neg_eq_add, smul_add,
+    Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, smul_eq_mul,
+    ite_mul, zero_mul, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, Finset.sum_const,
+    Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, Complex.ofReal_mul]
   ring
 
 /-- `⁅𝐇(ε), 𝐀(ε)ᵢ⁆ = iℏkε²(¾𝐫(ε)⁻⁵(𝐱ⱼ𝐋ᵢⱼ + 𝐋ᵢⱼ𝐱ⱼ) + 3iℏ/2 𝐫(ε)⁻⁵𝐱ᵢ + 𝐫(ε)⁻³𝐩ᵢ)` -/
@@ -719,7 +697,7 @@ private lemma sum_Lprx (hε : 0 < ε) :
     rw [angularMomentumOperator_antisymm j i, neg_comp, neg_comp, ← sub_eq_add_neg]
     rw [comp_assoc, comp_assoc, ← comp_sub]
     repeat rw [comp_eq_comp_sub_commute 𝐩[_] 𝐱[_], position_commutation_momentum]
-    rw [kroneckerDelta_symm j i, sub_sub_sub_cancel_right]
+    rw [symm j i, sub_sub_sub_cancel_right]
     rw [← angularMomentumOperator]
   rw [← angularMomentumOperatorSqr, ← sub_eq_zero]
   exact angularMomentumSqr_commutation_radiusRegPow hε
@@ -742,7 +720,7 @@ private lemma sum_prx (hε : 0 < ε) : ∑ i : Fin H.d, 𝐩[i] ∘L 𝐫[ε,-1]
     rw [← comp_assoc, comp_eq_comp_sub_commute 𝐩[_] 𝐫[ε,-1], radiusRegPow_commutation_momentum hε]
     rw [sub_comp, smul_comp, comp_assoc, comp_assoc]
     rw [comp_eq_comp_sub_commute 𝐩[_] 𝐱[_], position_commutation_momentum]
-    rw [kroneckerDelta_self]
+    rw [eq_one_of_same]
     rw [comp_sub, comp_smul, comp_id]
   repeat rw [Finset.sum_sub_distrib, ← Finset.smul_sum, ← comp_finset_sum]
   rw [positionOperatorSqr_eq hε, comp_sub, radiusRegPowOperator_comp_eq hε, comp_smul, comp_id]
@@ -751,7 +729,7 @@ private lemma sum_prx (hε : 0 < ε) : ∑ i : Fin H.d, 𝐩[i] ∘L 𝐫[ε,-1]
   simp only [ContinuousLinearMap.sub_apply, SchwartzMap.sub_apply, ContinuousLinearMap.smul_apply,
     SchwartzMap.smul_apply, ContinuousLinearMap.sum_apply, SchwartzMap.sum_apply]
   simp only [coe_comp', coe_sum', Function.comp_apply, Finset.sum_apply, map_sum,
-    SchwartzMap.sum_apply, mul_one, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
+    SchwartzMap.sum_apply, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
     nsmul_eq_mul, smul_eq_mul, Complex.ofReal_neg, Complex.ofReal_one, neg_mul, one_mul,
     sub_add_cancel, Complex.real_smul, Complex.ofReal_pow, sub_neg_eq_add]
   ring_nf