Sign Insert Some mul filter contracted of lt

lemma signInsertSome_mul_filter_contracted_of_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  rw [signInsertSome, signInsertSomeProd_eq_finset (hφj := hg.2) (hg := hg.1),    signInsertSomeCoef_eq_finset (hφj := hg.2), if_neg (by omega), ← map_mul, ← map_mul]  congr 1  rw [mul_eq_iff_eq_mul, ofFinset_union_disjoint]  swap  · /- Disjointness needed for `ofFinset_union_disjoint`. -/    rw [Finset.disjoint_filter]    intro j _ h    simp only [Nat.succ_eq_add_one, not_lt, not_and, not_forall, not_or, not_le]    intro h1    use h1    omega  rw [ofFinset_union, ← mul_eq_one_iff, 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 hn    simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,      hn, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, or_false,      true_and, and_self, Finset.mem_inter, not_and, not_lt, Classical.not_imp, not_le, and_imp]    intro h    rcases h with h | h    · simp only [h, or_true, isEmpty_Prop, not_le, IsEmpty.forall_iff, and_self]    · simp only [h, true_and]      refine And.intro ?_ (And.intro ?_ h.2)      · by_contra hkj        simp only [not_lt] at hkj        have h2 := h.2 hkj        apply Fin.ne_succAbove i j        have hij : i.succAbove j ≤ i.succAbove k.1 := Fin.succAbove_le_succAbove_iff.mpr hkj        omega      · have h1' := h.1        rcases h1' with h1' | h1'        · have hl := h.2 h1'          have hij : i.succAbove j ≤ i.succAbove k.1 := Fin.succAbove_le_succAbove_iff.mpr h1'          by_contra hn          apply Fin.ne_succAbove i j          omega        · exact h1'  · /- 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    simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,      hn, hj, forall_true_left, false_or, true_and, and_false, false_and, Finset.mem_inter,      not_false_eq_true, and_true, not_and, not_lt, getDual?_getDual?_get_get, reduceCtorEq,      Option.isSome_some, Option.get_some, forall_const, and_imp]    intro h1 h2    have hijsucc' : i.succAbove ((φsΛ.getDual? j).get hj) ≠ i := Fin.succAbove_ne i _    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    by_cases hik : ↑k < j    · have hn : ¬ j < ↑k := by omega      simp only [hik, true_and, hn, false_and, or_false, and_imp, and_true] at h1 h2 ⊢      have hir : i.succAbove j < i := by        rcases h1 with h1 | h1        · simp [h1]        · simp [h1]      simp only [hir, true_and, or_true, forall_const] at h1 h2      have hnkdual : ¬ ↑k < (φsΛ.getDual? j).get hj := by        by_contra hn        have h2 := h2 hn        apply Fin.ne_succAbove i j        omega      simp only [hnkdual, IsEmpty.forall_iff, false_and, false_or, and_imp] at h2 ⊢      have hnkdual : (φsΛ.getDual? j).get hj < ↑k := by omega      have hi : i.succAbove ((φsΛ.getDual? j).get hj) < i.succAbove k := by        rw [@Fin.succAbove_lt_succAbove_iff]        omega      omega    · have ht : j < ↑k := by omega      have ht' : i.succAbove j < i.succAbove k := by        rw [@Fin.succAbove_lt_succAbove_iff]        omega      simp only [hik, false_and, ht, true_and, false_or, and_false, or_false, and_imp] at h1 h2 ⊢      by_cases hik : i.succAbove j < i      · simp_all only [Fin.getElem_fin, ne_eq, not_lt, true_and, or_true]        have hn : ¬ i ≤ i.succAbove j := by omega        simp_all only [and_false, or_false, imp_false, not_lt, Nat.succ_eq_add_one, not_le]        apply And.intro        · apply Or.inr          omega        · intro h1 h2 h3          omega      · simp_all only [Fin.getElem_fin, ne_eq, not_lt, false_and, false_or, or_false, and_self,        or_true, imp_self]        omega