Lrl commutation lrl

lemma lrl_commutation_lrl (ε : ℝˣ) (i j : Fin H.d) :    ⁅H.lrlOperator ε i, H.lrlOperator ε j⁆ = ((-2 * I * ℏ * H.m) • H.hamiltonianRegCLM ε    + (I * ℏ * H.m * H.k * ε.1 ^ 2) • 𝐫₀ ε (-3)) ∘L 𝐋 i j := by  repeat rw [lrlOperator_eq]  let c₁ : ℂ := 2⁻¹ * I * ℏ * (H.d - 1)  let c₂ : ℂ := H.m * H.k  trans ⁅𝐱 i ∘L (𝐩 ⬝ᵥ 𝐩), 𝐱 j ∘L (𝐩 ⬝ᵥ 𝐩)⁆ + ⁅(𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 i, (𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 j⁆      + (c₂ ^ 2) • ⁅𝐫₀ ε (-1) ∘L 𝐱 i, 𝐫₀ ε (-1) ∘L 𝐱 j⁆      - (⁅𝐱 i ∘L (𝐩 ⬝ᵥ 𝐩), (𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 j⁆ + ⁅(𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 i, 𝐱 j ∘L (𝐩 ⬝ᵥ 𝐩)⁆)      + c₁ • (⁅𝐱 i ∘L (𝐩 ⬝ᵥ 𝐩), 𝐩 j⁆ + ⁅𝐩 i, 𝐱 j ∘L (𝐩 ⬝ᵥ 𝐩)⁆)      - c₂ • (⁅𝐱 i ∘L (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘L 𝐱 j⁆ + ⁅𝐫₀ ε (-1) ∘L 𝐱 i, 𝐱 j ∘L (𝐩 ⬝ᵥ 𝐩)⁆)      - c₁ • (⁅(𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 i, 𝐩 j⁆ + ⁅𝐩 i, (𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 j⁆)      + c₂ • (⁅(𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 i, 𝐫₀ ε (-1) ∘L 𝐱 j⁆ + ⁅𝐫₀ ε (-1) ∘L 𝐱 i, (𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 j⁆)      - (c₁ * c₂) • (⁅𝐩 i, 𝐫₀ ε (-1) ∘L 𝐱 j⁆ + ⁅𝐫₀ ε (-1) ∘L 𝐱 i, 𝐩 j⁆)  · simp only [lie_add, add_lie, lie_sub, sub_lie, lie_smul, smul_lie,      momentum_commutation_momentum, smul_zero, add_zero, ← Complex.coe_smul, ofReal_mul]    subst c₁ c₂    ext    simp only [sub_apply, add_apply, smul_apply, smul_eq_mul, smul_add]    ring  rw [positionCompMomentumSqr_comm, positionDotMomentumCompMomentum_comm,    positionCompMomentumSqr_comm_positionDotMomentumCompMomentum_add,    positionCompMomentumSqr_comm_momentum_add, positionDotMomentumCompMomentum_comm_momentum_add,    positionCompMomentumSqr_comm_radiusRegInvCompPosition_add,    positionDotMomentumCompMomentum_comm_radiusRegInvCompPosition_add,    momentum_comm_radiusRegInvCompPosition_add, radiusRegInvCompPosition_comm]  subst c₁ c₂  simp_rw [hamiltonianRegCLM_eq, smul_zero, add_zero, sub_zero, ← sub_smul, ← Complex.coe_smul,    ofReal_inv, ofReal_mul, ofReal_ofNat, smul_sub, smul_smul, add_comp, sub_comp, smul_comp]  ring_nf  simp