P P P! acc Cube

lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) :    accCubeTriLinSymm (P g) (P g) (basis!AsCharges j)    = g (j.succ) ^ 2 - g (j.castSucc) ^ 2 := by  simp only [succ_eq_add_one, accCubeTriLinSymm,    TriLinearSymm.mk₃_toFun_apply_apply]  erw [sum_evenShift, basis!_on_evenShiftZero, basis!_on_evenShiftLast]  simp only [mul_zero, add_zero, Function.comp_apply, zero_add]  rw [Fintype.sum_eq_single j, basis!_on_evenShiftFst_self, basis!_on_evenShiftSnd_self]  · simp only [evenShiftFst_eq_evenFst_succ, mul_one, evenShiftSnd_eq_evenSnd_castSucc, mul_neg]    rw [P_evenFst, P_evenSnd]    ring  · intro k hkj    erw [basis!_on_evenShiftFst_other hkj.symm, basis!_on_evenShiftSnd_other hkj.symm]    simp only [mul_zero, add_zero]