Sign Insert Some mul filter contracted of not lt

lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)    (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)    (hk : ¬ i.succAbove k < i) (hg : GradingCompliant φs φsΛ ∧ (𝓕 |>ₛ φ) = 𝓕 |>ₛ φs[k.1]) :    signInsertSome φ φs φsΛ i k *    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, φsΛ.uncontracted.filter (fun x => x < ↑k)⟩)    = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter (fun x => i.succAbove x < i)⟩) := by  have hik : i.succAbove ↑k ≠ i := Fin.succAbove_ne i ↑k  rw [signInsertSome, signInsertSomeProd_eq_finset (hφj := hg.2) (hg := hg.1),    signInsertSomeCoef_eq_finset (hφj := hg.2), if_pos (by omega), ← map_mul, ← map_mul]  congr 1  rw [mul_eq_iff_eq_mul, ofFinset_union, ofFinset_union]  apply (mul_eq_one_iff _ _).mp  rw [ofFinset_union]  simp only [Nat.succ_eq_add_one, not_lt]  apply stat_ofFinset_eq_one_of_gradingCompliant _ _ _ hg.1  · /- The `c.getDual? i = none` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/    intro j hj    have hijsucc : i.succAbove j ≠ i := Fin.succAbove_ne i j    simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,      hj, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, true_and,      and_false, or_false, Finset.mem_inter, not_false_eq_true, and_self, not_and, not_lt,      Classical.not_imp, not_le, and_imp]    intro h    have hij : i < i.succAbove j := by      rcases h with h | h      · exact h.1      · rcases h.1 with h1 | h1        · omega        · have hik : i.succAbove k.1 ≤ i.succAbove j := by            rw [Fin.succAbove_le_succAbove_iff]            omega          omega    simp only [hij, true_and] at h ⊢    omega  · /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/    intro j hj    have hn : ¬ φsΛ.getDual? j = none := Option.isSome_iff_ne_none.mp hj    have hijSuc : i.succAbove j ≠ i := Fin.succAbove_ne i j    have hkneqj : ↑k ≠ j := by      by_contra hkj      have hk := k.prop      simp only [uncontracted, Finset.mem_filter, Finset.mem_univ, true_and] at hk      simp_all    have hkneqgetdual : k.1 ≠ (φsΛ.getDual? j).get hj := by      by_contra hkj      have hk := k.prop      simp only [uncontracted, Finset.mem_filter, Finset.mem_univ, true_and] at hk      simp_all    simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,      hn, hj, forall_true_left, false_or, true_and, Finset.mem_inter, not_and, not_or, not_lt,      not_le, and_imp, and_false, false_and, not_false_eq_true, and_true, getDual?_getDual?_get_get,      reduceCtorEq, Option.isSome_some, Option.get_some, forall_const]    by_cases hik : ↑k < j    · have hikn : ¬ j < k.1 := by omega      have hksucc : i.succAbove k.1 < i.succAbove j := by        rw [Fin.succAbove_lt_succAbove_iff]        omega      have hkn : i < i.succAbove j := by omega      have hl : ¬ i.succAbove j < i := by omega      simp only [hkn, hikn, false_and, and_false, hl, false_or, or_self, IsEmpty.forall_iff,        imp_false, not_lt, true_and, implies_true, and_true, forall_const, hik,        imp_forall_iff_forall]    · have hikn : j < k.1 := by omega      have hksucc : i.succAbove j < i.succAbove k.1 := Fin.succAbove_lt_succAbove_iff.mpr hikn      simp only [hikn, true_and, forall_const, hik, false_and, or_false, IsEmpty.forall_iff,        and_true]      by_cases hij: i < i.succAbove j      · simp only [hij, true_and, forall_const, and_true, imp_forall_iff_forall]        have hijn : ¬ i.succAbove j < i := by omega        simp only [hijn, false_and, false_or, IsEmpty.forall_iff, imp_false, not_lt, true_and,          or_false, and_imp]        have hijle : i ≤ i.succAbove j := by omega        simp only [hijle, and_true, implies_true, forall_const]        intro h1 h2        apply And.intro        · rcases h1 with h1 | h1          · apply Or.inl            omega          · apply Or.inl            have hi : i.succAbove k.1 < i.succAbove ((φsΛ.getDual? j).get hj) :=              Fin.succAbove_lt_succAbove_iff.mpr h1            apply And.intro            · apply Or.inr              apply And.intro              · omega              · omega            · omega        · intro h3 h4          omega      · simp only [hij, false_and, false_or, IsEmpty.forall_iff, and_true, forall_const, and_false,        or_self, implies_true]        have hijn : i.succAbove j < i := by omega        have hijn' : ¬ i ≤ i.succAbove j := by omega        simp only [hijn, true_and, hijn', and_false, or_false, or_true, imp_false, not_lt,          forall_const]        exact fun h => lt_of_le_of_ne h (Fin.succAbove_ne i ((φsΛ.getDual? j).get hj))