Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Mathematics.List import all Physlib.Mathematics.List

List lemmas

@[expose] public sectionlemma insertionSortMin_lt_length_succ {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) : insertionSortMinPos r i l < (insertionSortDropMinPos r i l).length.succ := α:Typer:α → α → Propinst✝:DecidableRel ri:αl:List α⊢ ↑(insertionSortMinPos r i l) < (insertionSortDropMinPos r i l).length.succ All goals completed! 🐙

Given a list i :: l the left-most minimal position a of i :: l wrt r as an element of Fin (insertionSortDropMinPos r i l).length.succ.

def insertionSortMinPosFin {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) : Fin (insertionSortDropMinPos r i l).length.succ := ⟨insertionSortMinPos r i l, insertionSortMin_lt_length_succ r i l⟩
α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl:List αi:Fin (insertionSortDropMinPos r a l).lengthhl1:(∀ a' ∈ List.insertionSort r (insertionSortDropMinPos r a l), r (insertionSortMin r a l) a') ∧ List.Pairwise r (List.insertionSort r (insertionSortDropMinPos r a l))⊢ r (insertionSortMin r a l) (insertionSortDropMinPos r a l)[i] exact hl1.1 _ (α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl:List αi:Fin (insertionSortDropMinPos r a l).lengthhl1:(∀ a' ∈ List.insertionSort r (insertionSortDropMinPos r a l), r (insertionSortMin r a l) a') ∧ List.Pairwise r (List.insertionSort r (insertionSortDropMinPos r a l))⊢ (insertionSortDropMinPos r a l)[i] ∈ List.insertionSort r (insertionSortDropMinPos r a l) All goals completed! 🐙)α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List α⊢ (insertionSortEquiv r (a :: l)) ((insertionSortEquiv r (a :: l)).symm ⟨0, ⋯⟩) = ⟨0, ⋯⟩ All goals completed! 🐙lemma insertionSortEquiv_gt_zero_of_ne_insertionSortMinPos {α : Type} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) (k : Fin (a :: l).length) (hk : k ≠ insertionSortMinPos r a l) : ⟨0, n:ℕα:Typer:α → α → Propinst✝:DecidableRel ra:αl:List αk:Fin (a :: l).lengthhk:k ≠ insertionSortMinPos r a l⊢ 0 < (List.insertionSort r (a :: l)).length All goals completed! 🐙⟩ < insertionSortEquiv r (a :: l) k := α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List αk:Fin (a :: l).lengthhk:k ≠ insertionSortMinPos r a l⊢ ⟨0, ⋯⟩ < (insertionSortEquiv r (a :: l)) k α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List αk:Fin (a :: l).lengthhk:k ≠ insertionSortMinPos r a lhn:¬⟨0, ⋯⟩ < (insertionSortEquiv r (a :: l)) k⊢ False α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List αk:Fin (a :: l).lengthhk:k ≠ insertionSortMinPos r a lhn:(insertionSortEquiv r (a :: l)) k ≤ ⟨0, ⋯⟩⊢ False α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List αk:Fin (a :: l).lengthhk:k ≠ insertionSortMinPos r a lhn:(insertionSortEquiv r (a :: l)) k ≤ ⟨0, ⋯⟩⊢ (insertionSortEquiv r (a :: l)) k = ⟨0, ⋯⟩ α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List αk:Fin (a :: l).lengthhk:¬k = insertionSortMinPos r a lhn:↑((insertionSortEquiv r (a :: l)) k) = 0⊢ (insertionSortEquiv r (a :: l)) k = ⟨0, ⋯⟩ All goals completed! 🐙α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List αi:Fin (insertionSortDropMinPos r a l).lengthh:(insertionSortMinPosFin r a l).succAbove i < insertionSortMinPosFin r a lh1:(insertionSortDropMinPos r a l)[↑i] = (a :: l).get ((finCongr ⋯) ((insertionSortMinPosFin r a l).succAbove i))hl:↑(insertionSortMinPos r a l) = ↑(insertionSortMinPosFin r a l)⊢ ¬↑((insertionSortMinPosFin r a l).succAbove i) = ↑(insertionSortMinPos r a l) α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List αi:Fin (insertionSortDropMinPos r a l).lengthh:(insertionSortMinPosFin r a l).succAbove i < insertionSortMinPosFin r a lh1:(insertionSortDropMinPos r a l)[↑i] = (a :: l).get ((finCongr ⋯) ((insertionSortMinPosFin r a l).succAbove i))hl:↑(insertionSortMinPos r a l) = ↑(insertionSortMinPosFin r a l)⊢ ¬(insertionSortMinPosFin r a l).succAbove i = insertionSortMinPosFin r a l All goals completed! 🐙lemma insertionSort_insertionSort {α : Type} (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] (l1 : List α) : List.insertionSort r (List.insertionSort r l1) = List.insertionSort r l1 := α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α rl1:List α⊢ List.insertionSort r (List.insertionSort r l1) = List.insertionSort r l1 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α rl1:List α⊢ List.Pairwise r (List.insertionSort r l1) All goals completed! 🐙α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:r a c⊢ List.orderedInsert r a (b :: c :: l) = b :: a :: c :: l All goals completed! 🐙 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a c⊢ List.orderedInsert r a (if r b c then b :: c :: l else c :: List.orderedInsert r b l) = List.orderedInsert r b (if r a c then a :: c :: l else c :: List.orderedInsert r a l) α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a c⊢ List.orderedInsert r a (if r b c then b :: c :: l else c :: List.orderedInsert r b l) = if r b c then b :: c :: List.orderedInsert r a l else c :: List.orderedInsert r b (List.orderedInsert r a l) α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a chbc:r b c⊢ List.orderedInsert r a (if r b c then b :: c :: l else c :: List.orderedInsert r b l) = if r b c then b :: c :: List.orderedInsert r a l else c :: List.orderedInsert r b (List.orderedInsert r a l)α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a chbc:¬r b c⊢ List.orderedInsert r a (if r b c then b :: c :: l else c :: List.orderedInsert r b l) = if r b c then b :: c :: List.orderedInsert r a l else c :: List.orderedInsert r b (List.orderedInsert r a l) α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a chbc:r b c⊢ List.orderedInsert r a (if r b c then b :: c :: l else c :: List.orderedInsert r b l) = if r b c then b :: c :: List.orderedInsert r a l else c :: List.orderedInsert r b (List.orderedInsert r a l) All goals completed! 🐙 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a chbc:¬r b c⊢ List.orderedInsert r a (if r b c then b :: c :: l else c :: List.orderedInsert r b l) = if r b c then b :: c :: List.orderedInsert r a l else c :: List.orderedInsert r b (List.orderedInsert r a l) α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a chbc:¬r b c⊢ List.orderedInsert r a (List.orderedInsert r b l) = List.orderedInsert r b (List.orderedInsert r a l) All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙@[simp] lemma orderedInsert_length {α : Type} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) : (List.orderedInsert r a l).length = (a :: l).length := α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List α⊢ (List.orderedInsert r a l).length = (a :: l).length α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List α⊢ (List.orderedInsert r a l).Perm (a :: l) All goals completed! 🐙lemma takeWhile_orderedInsert {α : Type} (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] (a b : α) (hr : ¬ r a b) : (l : List α) → (List.takeWhile (fun c => !decide (r a c)) (List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) l).length + 1 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a b⊢ (List.takeWhile (fun c => !decide (r a c)) (List.orderedInsert r b [])).length = (List.takeWhile (fun c => !decide (r a c)) []).length + 1 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a b⊢ (List.takeWhile (fun c => !decide (r a c)) (List.orderedInsert r b [])).length = (List.takeWhile (fun c => !decide (r a c)) []).length + 1 All goals completed! 🐙 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List α⊢ (List.takeWhile (fun c => !decide (r a c)) (List.orderedInsert r b (c :: l))).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List α⊢ (List.takeWhile (fun c => !decide (r a c)) (List.orderedInsert r b (c :: l))).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List α⊢ (List.takeWhile (fun c => !decide (r a c)) (if r b c then b :: c :: l else c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:r b c⊢ (List.takeWhile (fun c => !decide (r a c)) (if r b c then b :: c :: l else c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:¬r b c⊢ (List.takeWhile (fun c => !decide (r a c)) (if r b c then b :: c :: l else c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:r b c⊢ (List.takeWhile (fun c => !decide (r a c)) (if r b c then b :: c :: l else c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 All goals completed! 🐙 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:¬r b c⊢ (List.takeWhile (fun c => !decide (r a c)) (if r b c then b :: c :: l else c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:¬r b c⊢ (List.takeWhile (fun c => !decide (r a c)) (c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:¬r b chl:¬r a c⊢ (List.takeWhile (fun c => !decide (r a c)) (c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:¬r b chl:¬r a c⊢ (List.takeWhile (fun c => !decide (r a c)) (List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) l).length + 1 All goals completed! 🐙lemma takeWhile_orderedInsert' {α : Type} (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] (a b : α) (hr : ¬ r a b) : (l : List α) → (List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) l).length α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a b⊢ (List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a [])).length = (List.takeWhile (fun c => !decide (r b c)) []).length α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a b⊢ (List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a [])).length = (List.takeWhile (fun c => !decide (r b c)) []).length All goals completed! 🐙 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List α⊢ (List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a (c :: l))).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List α⊢ (List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a (c :: l))).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b a⊢ (List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a (c :: l))).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b a⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:r b c⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).lengthα:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b c⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:r b c⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:r b chac:r a c⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).lengthα:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:r b chac:¬r a c⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:r b chac:r a c⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).lengthα:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:r b chac:¬r a c⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length All goals completed! 🐙 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b c⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b chac:r a c⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).lengthα:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b chac:¬r a c⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b chac:r a c⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length All goals completed! 🐙 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b chac:¬r a c⊢ (List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b chac:¬r a c⊢ (List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) l).length All goals completed! 🐙α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1⊢ ↑(a1.succAbove ⟨↑(b1.succAbove n), ⋯⟩) = ↑(b2.succAbove ⟨↑(a2.succAbove n), ⋯⟩) α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1⊢ (if (if ↑n < ↑b2 then ↑n else ↑n + 1) < ↑a2 + 1 then if ↑n < ↑b2 then ↑n else ↑n + 1 else (if ↑n < ↑b2 then ↑n else ↑n + 1) + 1) = if (if ↑n < ↑a2 then ↑n else ↑n + 1) < ↑b2 then if ↑n < ↑a2 then ↑n else ↑n + 1 else (if ↑n < ↑a2 then ↑n else ↑n + 1) + 1 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝²:↑n < ↑b2h✝¹:↑n < ↑a2 + 1h✝:↑n < ↑a2⊢ ↑n = ↑nα:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:↑n < ↑b2h✝²:↑n < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:↑n + 1 < ↑b2⊢ ↑n = ↑n + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:↑n < ↑b2h✝²:↑n < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:¬↑n + 1 < ↑b2⊢ ↑n = ↑n + 1 + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝²:↑n < ↑b2h✝¹:¬↑n < ↑a2 + 1h✝:↑n < ↑a2⊢ ↑n + 1 = ↑nα:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:↑n < ↑b2h✝²:¬↑n < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:↑n + 1 < ↑b2⊢ ↑n + 1 = ↑n + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:↑n < ↑b2h✝²:¬↑n < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:¬↑n + 1 < ↑b2⊢ ↑n + 1 = ↑n + 1 + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝²:¬↑n < ↑b2h✝¹:↑n + 1 < ↑a2 + 1h✝:↑n < ↑a2⊢ ↑n + 1 = ↑n + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:¬↑n < ↑b2h✝²:↑n + 1 < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:↑n + 1 < ↑b2⊢ ↑n + 1 = ↑n + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:¬↑n < ↑b2h✝²:↑n + 1 < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:¬↑n + 1 < ↑b2⊢ ↑n + 1 = ↑n + 1 + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝²:¬↑n < ↑b2h✝¹:¬↑n + 1 < ↑a2 + 1h✝:↑n < ↑a2⊢ ↑n + 1 + 1 = ↑n + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:¬↑n < ↑b2h✝²:¬↑n + 1 < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:↑n + 1 < ↑b2⊢ ↑n + 1 + 1 = ↑n + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:¬↑n < ↑b2h✝²:¬↑n + 1 < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:¬↑n + 1 < ↑b2⊢ ↑n + 1 + 1 = ↑n + 1 + 1 α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝²:↑n < ↑b2h✝¹:↑n < ↑a2 + 1h✝:↑n < ↑a2⊢ ↑n = ↑nα:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:↑n < ↑b2h✝²:↑n < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:↑n + 1 < ↑b2⊢ ↑n = ↑n + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:↑n < ↑b2h✝²:↑n < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:¬↑n + 1 < ↑b2⊢ ↑n = ↑n + 1 + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝²:↑n < ↑b2h✝¹:¬↑n < ↑a2 + 1h✝:↑n < ↑a2⊢ ↑n + 1 = ↑nα:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:↑n < ↑b2h✝²:¬↑n < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:↑n + 1 < ↑b2⊢ ↑n + 1 = ↑n + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:↑n < ↑b2h✝²:¬↑n < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:¬↑n + 1 < ↑b2⊢ ↑n + 1 = ↑n + 1 + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝²:¬↑n < ↑b2h✝¹:↑n + 1 < ↑a2 + 1h✝:↑n < ↑a2⊢ ↑n + 1 = ↑n + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:¬↑n < ↑b2h✝²:↑n + 1 < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:↑n + 1 < ↑b2⊢ ↑n + 1 = ↑n + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:¬↑n < ↑b2h✝²:↑n + 1 < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:¬↑n + 1 < ↑b2⊢ ↑n + 1 = ↑n + 1 + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝²:¬↑n < ↑b2h✝¹:¬↑n + 1 < ↑a2 + 1h✝:↑n < ↑a2⊢ ↑n + 1 + 1 = ↑n + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:¬↑n < ↑b2h✝²:¬↑n + 1 < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:↑n + 1 < ↑b2⊢ ↑n + 1 + 1 = ↑n + 1α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:ℕhrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), ⋯⟩b1:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) b), ⋯⟩a2:Fin ((List.insertionSort r l).length + 1) := ⟨↑(orderedInsertPos r (List.insertionSort r l) a), ⋯⟩b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := ⟨↑(orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ⋯⟩ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:↑b1 ≤ ↑a2ha2:↑a1 = ↑a2 + 1hb:↑b1 = ↑b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) ⟨n✝, ⋯⟩hba:↑b2 ≤ ↑a2val_succAbove:∀ {m : ℕ} (p : Fin (m + 1)) (i : Fin m), ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1h✝³:¬↑n < ↑b2h✝²:¬↑n + 1 < ↑a2 + 1h✝¹:¬↑n < ↑a2h✝:¬↑n + 1 < ↑b2⊢ ↑n + 1 + 1 = ↑n + 1 + 1 All goals completed! 🐙α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αa2:αb:αl1:List αl2:List αh:¬r a bh1:List.orderedInsert r a (b :: l1) ++ a2 :: l2 = b :: List.orderedInsert r a l1 ++ a2 :: l2hl✝:List.insertionSort r (List.orderedInsert r a l1 ++ a2 :: l2) = List.insertionSort r (a :: l1 ++ a2 :: l2)hl:l1.length + 1 + 1 = l1.length + 2⊢ Fin.cast ⋯ ((insertionSortEquiv r (b :: a :: (l1 ++ a2 :: l2))) ⟨l1.length + 2, ⋯⟩) = Fin.cast ⋯ ((insertionSortEquiv r (a :: b :: (l1 ++ a2 :: l2))) ⟨l1.length + 1 + 1, ⋯⟩) α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αa2:αb:αl1:List αl2:List αh:¬r a bh1:List.orderedInsert r a (b :: l1) ++ a2 :: l2 = b :: List.orderedInsert r a l1 ++ a2 :: l2hl✝:List.insertionSort r (List.orderedInsert r a l1 ++ a2 :: l2) = List.insertionSort r (a :: l1 ++ a2 :: l2)hl:l1.length + 1 + 1 = l1.length + 2⊢ Fin.cast ⋯ ((insertionSortEquiv r (b :: a :: (l1 ++ a2 :: l2))) ⟨l1.length + 2, ⋯⟩) = Fin.cast ⋯ ((insertionSortEquiv r (a :: b :: (l1 ++ a2 :: l2))) ⟨l1.length + 2, ⋯⟩) conv_rhs => α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αa2:αb:αl1:List αl2:List αh:¬r a bh1:List.orderedInsert r a (b :: l1) ++ a2 :: l2 = b :: List.orderedInsert r a l1 ++ a2 :: l2hl✝:List.insertionSort r (List.orderedInsert r a l1 ++ a2 :: l2) = List.insertionSort r (a :: l1 ++ a2 :: l2)hl:l1.length + 1 + 1 = l1.length + 2| Fin.cast ⋯ ((finCongr ⋯) ((insertionSortEquiv r (b :: a :: (l1 ++ a2 :: l2))) ⟨l1.length + 2, ⋯⟩)) α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αa2:αb:αl1:List αl2:List αh:¬r a bh1:List.orderedInsert r a (b :: l1) ++ a2 :: l2 = b :: List.orderedInsert r a l1 ++ a2 :: l2hl✝:List.insertionSort r (List.orderedInsert r a l1 ++ a2 :: l2) = List.insertionSort r (a :: l1 ++ a2 :: l2)hl:l1.length + 1 + 1 = l1.length + 2⊢ (insertionSortEquiv r (b :: a :: (l1 ++ a2 :: l2))) ⟨l1.length + 2, ⋯⟩ = (insertionSortEquiv r (b :: a :: (l1 ++ a2 :: l2))) ⟨l1.length + 2, ⋯⟩ All goals completed! 🐙α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl1:List αl2:List αhl✝:(insertionSortEquiv r (List.orderedInsert r b (List.insertionSort r l1) ++ a :: l2)) ⟨l1.length + 1, ⋯⟩ = Fin.cast ⋯ ((insertionSortEquiv r (b :: (List.insertionSort r l1 ++ a :: l2))) ⟨l1.length + 1, ⋯⟩)ih:(insertionSortEquiv r (List.insertionSort r l1 ++ a :: l2)) ⟨l1.length, ⋯⟩ = (finCongr ⋯) ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩)hl:List.insertionSort r (List.insertionSort r l1 ++ a :: l2) = List.insertionSort r (l1 ++ a :: l2)⊢ Fin.cast ⋯ ((orderedInsertEquiv r (List.foldr (List.orderedInsert r) [] (List.foldr (List.orderedInsert r) [] l1 ++ a :: l2)) b) ((finCongr ⋯) ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩)).succ) = Fin.cast ⋯ ((orderedInsertEquiv r (List.foldr (List.orderedInsert r) [] (l1 ++ a :: l2)) b) ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩).succ) erw [α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl1:List αl2:List αhl✝:(insertionSortEquiv r (List.orderedInsert r b (List.insertionSort r l1) ++ a :: l2)) ⟨l1.length + 1, ⋯⟩ = Fin.cast ⋯ ((insertionSortEquiv r (b :: (List.insertionSort r l1 ++ a :: l2))) ⟨l1.length + 1, ⋯⟩)ih:(insertionSortEquiv r (List.insertionSort r l1 ++ a :: l2)) ⟨l1.length, ⋯⟩ = (finCongr ⋯) ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩)hl:List.insertionSort r (List.insertionSort r l1 ++ a :: l2) = List.insertionSort r (l1 ++ a :: l2)⊢ Fin.cast ⋯ (((Fin.castOrderIso ⋯).trans ((orderedInsertEquiv r (List.insertionSort r (l1 ++ a :: l2)) b).trans (Fin.castOrderIso ⋯).toEquiv)) ((finCongr ⋯) ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩)).succ) = Fin.cast ⋯ ((orderedInsertEquiv r (List.foldr (List.orderedInsert r) [] (l1 ++ a :: l2)) b) ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩).succ)α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl1:List αl2:List αhl✝:(insertionSortEquiv r (List.orderedInsert r b (List.insertionSort r l1) ++ a :: l2)) ⟨l1.length + 1, ⋯⟩ = Fin.cast ⋯ ((insertionSortEquiv r (b :: (List.insertionSort r l1 ++ a :: l2))) ⟨l1.length + 1, ⋯⟩)ih:(insertionSortEquiv r (List.insertionSort r l1 ++ a :: l2)) ⟨l1.length, ⋯⟩ = (finCongr ⋯) ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩)hl:List.insertionSort r (List.insertionSort r l1 ++ a :: l2) = List.insertionSort r (l1 ++ a :: l2)⊢ Fin.cast ⋯ (((Fin.castOrderIso ⋯).trans ((orderedInsertEquiv r (List.insertionSort r (l1 ++ a :: l2)) b).trans (Fin.castOrderIso ⋯).toEquiv)) ((finCongr ⋯) ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩)).succ) = Fin.cast ⋯ ((orderedInsertEquiv r (List.foldr (List.orderedInsert r) [] (l1 ++ a :: l2)) b) ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩).succ) α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl1:List αl2:List αhl✝:(insertionSortEquiv r (List.orderedInsert r b (List.insertionSort r l1) ++ a :: l2)) ⟨l1.length + 1, ⋯⟩ = Fin.cast ⋯ ((insertionSortEquiv r (b :: (List.insertionSort r l1 ++ a :: l2))) ⟨l1.length + 1, ⋯⟩)ih:(insertionSortEquiv r (List.insertionSort r l1 ++ a :: l2)) ⟨l1.length, ⋯⟩ = (finCongr ⋯) ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩)hl:List.insertionSort r (List.insertionSort r l1 ++ a :: l2) = List.insertionSort r (l1 ++ a :: l2)⊢ Fin.cast ⋯ (((Fin.castOrderIso ⋯).trans ((orderedInsertEquiv r (List.insertionSort r (l1 ++ a :: l2)) b).trans (Fin.castOrderIso ⋯).toEquiv)) (Fin.cast ⋯ ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩)).succ) = Fin.cast ⋯ ((orderedInsertEquiv r (List.foldr (List.orderedInsert r) [] (l1 ++ a :: l2)) b) ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩).succ) All goals completed! 🐙

Insertion sort with equal fields

α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:IsTrans α ra:αp:α → Propinst✝:DecidablePred ph:p ab:αl:List αhl:List.Pairwise r (b :: l)hpb:¬p bhab:¬r a b⊢ List.filter (fun b => decide (p b)) (List.orderedInsert r a l) = List.orderedInsert r a (List.filter (fun b => decide (p b)) l) α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:IsTrans α ra:αp:α → Propinst✝:DecidablePred ph:p ab:αl:List αhpb:¬p bhab:¬r a bhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r l⊢ List.filter (fun b => decide (p b)) (List.orderedInsert r a l) = List.orderedInsert r a (List.filter (fun b => decide (p b)) l) All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙lemma takeWhile_sorted_eq_filter {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] (a : α) : (l : List α) → (hl : l.Pairwise r) → List.takeWhile (fun c => ¬ r a c) l = List.filter (fun c => ¬ r a c) l α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αx✝:List.Pairwise r []⊢ List.takeWhile (fun c => decide ¬r a c) [] = List.filter (fun c => decide ¬r a c) [] α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αx✝:List.Pairwise r []⊢ List.takeWhile (fun c => decide ¬r a c) [] = List.filter (fun c => decide ¬r a c) [] All goals completed! 🐙 α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:List.Pairwise r (b :: l)⊢ List.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l) α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:List.Pairwise r (b :: l)⊢ List.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l) α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r l⊢ List.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l) α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r lhb:¬r a b⊢ List.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l)α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r lhb:¬¬r a b⊢ List.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l) α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r lhb:¬r a b⊢ List.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l) α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r lhb:¬r a b⊢ List.takeWhile (fun c => !decide (r a c)) l = List.filter (fun c => !decide (r a c)) l All goals completed! 🐙 α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r lhb:¬¬r a b⊢ List.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l) α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r lhb:r a b⊢ ∀ a_1 ∈ l, r a a_1 All goals completed! 🐙α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r lhb:r a b⊢ ∀ a_1 ∈ l, decide (r a a_1) = true α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r lhb:r a bc:αhc:c ∈ l⊢ decide (r a c) = true All goals completed! 🐙α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r lhb:r a bhba:¬r b ah1:List.filter (fun c => decide (r a c) && decide (r c a)) l = []⊢ (decide (r a b) && !decide (r b a)) = trueα:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r lhb:r a bhba:¬r b ah1:List.filter (fun c => decide (r a c) && decide (r c a)) l = []⊢ List.Pairwise r l α:Typer:α → α → Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' ∈ l, r b a') ∧ List.Pairwise r lhb:r a bhba:¬r b ah1:List.filter (fun c => decide (r a c) && decide (r c a)) l = []⊢ List.Pairwise r l All goals completed! 🐙α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl:List αh:¬(r a b ∧ r b a)hl:List.filter (fun b => decide (r a b) && decide (r b a)) (List.orderedInsert r b (List.insertionSort r l)) = List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l)⊢ List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l) = List.filter (fun c => decide (r a c) && decide (r c a)) lα:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl:List αh:¬(r a b ∧ r b a)hl:List.filter (fun b => decide (r a b) && decide (r b a)) (List.orderedInsert r b (List.insertionSort r l)) = List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l)⊢ ¬(decide (r a b) && decide (r b a)) = true α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl:List αh:¬(r a b ∧ r b a)hl:List.filter (fun b => decide (r a b) && decide (r b a)) (List.orderedInsert r b (List.insertionSort r l)) = List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l)ih:List.filter (fun c => decide (r a c ∧ r c a)) (List.insertionSort r l) = List.filter (fun c => decide (r a c ∧ r c a)) l⊢ List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l) = List.filter (fun c => decide (r a c) && decide (r c a)) lα:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl:List αh:¬(r a b ∧ r b a)hl:List.filter (fun b => decide (r a b) && decide (r b a)) (List.orderedInsert r b (List.insertionSort r l)) = List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l)⊢ ¬(decide (r a b) && decide (r b a)) = true α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl:List αh:¬(r a b ∧ r b a)hl:List.filter (fun b => decide (r a b) && decide (r b a)) (List.orderedInsert r b (List.insertionSort r l)) = List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l)⊢ ¬(decide (r a b) && decide (r b a)) = true All goals completed! 🐙α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl:List αl2:List αh:∀ b ∈ l, r a b ∧ r b ahlt:List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l ++ l2)) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2))h1✝:List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) → List.dropWhile (fun c => !decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2))) = List.filter (fun c => decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2)))h1:List.insertionSort r (List.filter (fun b => decide (r a b) && !decide (r b a)) l1 ++ (List.filter (fun b => decide (r a b) && !decide (r b a)) l ++ List.filter (fun b => decide (r a b) && !decide (r b a)) l2)) = List.filter (fun b => decide (r a b) && !decide (r b a)) (List.insertionSort r (l1 ++ (l ++ l2)))h2:List.insertionSort r (List.filter (fun b => decide (r a b) && !decide (r b a)) l1 ++ List.filter (fun b => decide (r a b) && !decide (r b a)) l2) = List.filter (fun b => decide (r a b) && !decide (r b a)) (List.insertionSort r (l1 ++ l2))hl:List.filter (fun b => decide (r a b) && !decide (r b a)) l = []⊢ [] ++ List.filter (fun b => decide (r a b) && !decide (r b a)) l2 = List.filter (fun b => decide (r a b) && !decide (r b a)) l2α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl:List αl2:List αh:∀ b ∈ l, r a b ∧ r b ahlt:List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l ++ l2)) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2))h1:List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) → List.dropWhile (fun c => !decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2))) = List.filter (fun c => decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2)))⊢ List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2)))α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl:List αl2:List αh:∀ b ∈ l, r a b ∧ r b ahlt:List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l ++ l2)) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2))h1:List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) → List.dropWhile (fun c => !decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2))) = List.filter (fun c => decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2)))⊢ List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl:List αl2:List αh:∀ b ∈ l, r a b ∧ r b ahlt:List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l ++ l2)) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2))h1:List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) → List.dropWhile (fun c => !decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2))) = List.filter (fun c => decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2)))⊢ List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2)))α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl:List αl2:List αh:∀ b ∈ l, r a b ∧ r b ahlt:List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l ++ l2)) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2))h1:List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) → List.dropWhile (fun c => !decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2))) = List.filter (fun c => decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2)))⊢ List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl:List αl2:List αh:∀ b ∈ l, r a b ∧ r b ahlt:List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l ++ l2)) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2))h1:List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) → List.dropWhile (fun c => !decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2))) = List.filter (fun c => decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2)))⊢ List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) All goals completed! 🐙lemma insertionSort_of_takeWhile_filter {α : Type} (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] (a : α) (l1 l2 : List α) : List.insertionSort r (l1 ++ l2) = (List.takeWhile (fun c => ¬ r a c) ((l1 ++ l2).insertionSort r)) ++ (List.filter (fun c => r a c ∧ r c a) l1) ++ (List.filter (fun c => r a c ∧ r c a) l2) ++ (List.filter (fun c => r a c ∧ ¬ r c a) ((l1 ++ l2).insertionSort r)) := α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl2:List α⊢ List.insertionSort r (l1 ++ l2) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2)) ++ List.filter (fun c => decide (r a c ∧ r c a)) l1 ++ List.filter (fun c => decide (r a c ∧ r c a)) l2 ++ List.filter (fun c => decide (r a c ∧ ¬r c a)) (List.insertionSort r (l1 ++ l2)) simpa using insertionSort_of_eq_list r a l1 [] l2 (α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl2:List α⊢ ∀ b ∈ [], r a b ∧ r b a All goals completed! 🐙)