Pure prod P assoc

lemma Pure.prodP_assoc' {n n1 n2} {c : Fin n → C}    {c1 : Fin n1 → C} {c2 : Fin n2 → C}    (p : Pure S c) (p1 : Pure S c1) (p2 : Pure S c2) :    prodP p (prodP p1 p2) = permP _ IsReindexing.append_assoc_left (prodP (prodP p p1) p2) := by  ext i  refine Fin.addCases (fun i => ?_) (fun i => Fin.addCases (fun i => ?_) (fun i => ?_) i) i  · have h0 : (i.castAdd (n1 + n2)).cast (by grind) = (i.castAdd n1).castAdd n2 := by grind    simp [permP, ← congr_right _ _ _ h0]  · have h0 : ((i.castAdd n2).natAdd n).cast (by grind) = (i.natAdd n).castAdd n2 := by grind    simp [permP, ← congr_right _ _ _ h0]  · have h0 : ((i.natAdd n1).natAdd n).cast (by grind) = i.natAdd (n + n1) := by grind    simp [permP, ← congr_right _ _ _ h0]