Insert And Contract Nat erase

@[simp]lemma insertAndContractNat_erase (c : WickContraction n) (i : Fin n.succ)    (j : Option c.uncontracted) : erase (insertAndContractNat c i j) i = c := by  refine Subtype.ext (Finset.ext fun a => ?_)  simp only [erase, Nat.succ_eq_add_one, insertAndContractNat, Finset.mem_filter, Finset.mem_univ,    true_and]  match j with  | none =>    simp [Finset.mapEmbedding_apply, Finset.map_inj]  | some j =>    have hn : Finset.map i.succAboveEmb a ≠ {i, i.succAbove j} := fun h => by      have hi : i ∈ Finset.map i.succAboveEmb a := h ▸ Finset.mem_insert_self i _      simp [Fin.succAbove_ne] at hi    simp [Finset.mapEmbedding_apply, Finset.map_inj, hn]