Lrl Operator Sqr eq

lemma lrlOperatorSqr_eq (ε : ℝˣ) : H.lrlOperator ε ⬝ᵥ H.lrlOperator ε =    (2 * H.m) • (H.hamiltonianRegCLM ε) ∘L      (𝐋² + (4⁻¹ * ℏ ^ 2 * (H.d - 1) ^ 2 : ℝ) • ContinuousLinearMap.id ℂ 𝓢(Space H.d, ℂ))    + (H.m ^ 2 * H.k ^ 2) • (ContinuousLinearMap.id ℂ 𝓢(Space H.d, ℂ) - ε.1 ^ 2 • 𝐫₀ ε (-2))    - (2⁻¹ * ℏ^2 * H.m * H.k * (H.d - 1) * ε.1 ^ 2) • 𝐫₀ ε (-3) := by  simp_rw [dotProduct, mul_def]  conv_lhs => enter [2, i, 1]; rw [lrlOperator_eq']  conv_lhs => enter [2, i, 2]; rw [lrlOperator_eq'']  simp_rw [dotProduct, mul_def, sub_eq_add_neg, ← neg_smul, add_comp, comp_add, smul_comp,    comp_smul, finsetSum_comp, comp_finsetSum, Finset.sum_add_distrib, ← Finset.smul_sum,    comp_assoc, sum_LppL, sum_Lpp, sum_Lprx, sum_ppL, sum_prx, sum_rxpL, sum_rxp, sum_rxrx]  simp only [dotProduct, mul_def, ← neg_mul, smul_zero, add_zero, ← Complex.coe_smul, ofReal_mul,    ofReal_neg, smul_smul, zero_add, sub_eq_add_neg, ← neg_smul, smul_add, ofReal_pow,    hamiltonianRegCLM_eq, ofReal_inv, ofReal_ofNat]  ring_nf  ext  simp only [add_apply, _root_.smul_apply, _root_.add_apply,    _root_.smul_apply, Function.comp_apply, coe_comp, coe_id', smul_eq_mul, ofReal_add,    ofReal_neg, ofReal_one, ofReal_natCast]  grind [I_sq, H.m_ne_zero, mul_inv_cancel₀, ofReal_eq_zero]