Ordered Insert filter of pos

lemma orderedInsert_filter_of_pos {α : Type} (r : α → α → Prop) [DecidableRel r]    [IsTrans α r] (a : α) (p : α → Prop) [DecidablePred p] (h : p a) : (l : List α) →    (hl : l.Pairwise r) →    List.filter p (List.orderedInsert r a l) = List.orderedInsert r a (List.filter p l)  | [], hl => by    simp only [List.orderedInsert, List.filter_nil, List.orderedInsert_nil, List.filter_eq_self,      List.mem_singleton, decide_eq_true_eq, forall_eq]    exact h  | b :: l, hl => by    simp only [List.orderedInsert]    by_cases hpb : p b <;> by_cases hab : r a b    · simp only [hab, ↓reduceIte, hpb, decide_true, List.filter_cons_of_pos,      List.orderedInsert.eq_2]      rw [List.filter_cons_of_pos (by simp [h])]      rw [List.filter_cons_of_pos (by simp [hpb])]    · simp only [hab, ↓reduceIte]      rw [List.filter_cons_of_pos (by simp [hpb])]      rw [List.filter_cons_of_pos (by simp [hpb])]      simp only [List.orderedInsert, hab, ↓reduceIte, List.cons.injEq, true_and]      simp only [List.pairwise_cons] at hl      exact orderedInsert_filter_of_pos r a p h l hl.2    · simp only [hab, ↓reduceIte]      rw [List.filter_cons_of_pos (by simp [h]),        List.filter_cons_of_neg (by simp [hpb])]      rw [List.orderedInsert_eq_take_drop]      have hl : List.takeWhile (fun b => decide ¬r a b)          (List.filter (fun b => decide (p b)) l) = [] := by        rw [List.takeWhile_eq_nil_iff]        intro c hc        simp only [List.get_eq_getElem, decide_not, Bool.not_eq_eq_eq_not, Bool.not_true,          decide_eq_false_iff_not] at hc        apply hc        apply IsTrans.trans a b _ hab        simp only [List.pairwise_cons] at hl        exact hl.1 _ (List.mem_filter.mp (List.getElem_mem c)).1      rw [hl]      simp only [decide_not, List.nil_append, List.cons.injEq, true_and]      conv_lhs => rw [← List.takeWhile_append_dropWhile (p := fun b => decide ¬r a b)        (l := List.filter (fun b => decide (p b)) l)]      rw [hl]      simp    · simp only [hab, ↓reduceIte]      rw [List.filter_cons_of_neg (by simp [hpb])]      rw [List.filter_cons_of_neg (by simp [hpb])]      simp only [List.pairwise_cons] at hl      exact orderedInsert_filter_of_pos r a p h l hl.2