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.Fin public import Mathlib.Order.Lattice.Nat public import Mathlib.Data.List.TakeWhile import all Mathlib.Data.List.Sort

List lemmas

I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List Ih:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPb:P bhPa:P a⊢ List.takeWhile (fun b => decide (P b)) (a :: b :: l).tail = (match decide (P a) with | true => a :: match decide (P b) with | true => b :: List.takeWhile (fun b => decide (P b)) l | false => [] | false => []).tail All goals completed! 🐙 I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List Ih:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPb:¬P b⊢ List.takeWhile (fun b => decide (P b)) (a :: b :: l).tail = (match decide (P a) with | true => a :: match decide (P b) with | true => b :: List.takeWhile (fun b => decide (P b)) l | false => [] | false => []).tail I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List Ih:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPb:¬P b⊢ (match decide (P a) with | true => [a] | false => []).tail = [] I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List Ih:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPb:¬P bx✝:Boolheq✝:decide (P a) = true⊢ [a].tail = []I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List Ih:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPb:¬P bx✝:Boolheq✝:decide (P a) = false⊢ [].tail = [] I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List Ih:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPb:¬P bx✝:Boolheq✝:decide (P a) = true⊢ [a].tail = []I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List Ih:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPb:¬P bx✝:Boolheq✝:decide (P a) = false⊢ [].tail = [] All goals completed! 🐙 I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)⊢ List.takeWhile (fun b => decide (P b)) ((a :: b :: l).eraseIdx n.succ) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx n.succ I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)⊢ List.takeWhile (fun b => decide (P b)) ((a :: b :: l).eraseIdx n.succ) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx n.succ I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)⊢ List.takeWhile (fun b => decide (P b)) (a :: (b :: l).eraseIdx n) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx (n + 1) I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPa:P a⊢ List.takeWhile (fun b => decide (P b)) (a :: (b :: l).eraseIdx n) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx (n + 1)I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPa:¬P a⊢ List.takeWhile (fun b => decide (P b)) (a :: (b :: l).eraseIdx n) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx (n + 1) I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPa:P a⊢ List.takeWhile (fun b => decide (P b)) (a :: (b :: l).eraseIdx n) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx (n + 1) I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPa:P a⊢ (match decide (P a) with | true => a :: List.takeWhile (fun b => decide (P b)) ((b :: l).eraseIdx n) | false => []) = (match decide (P a) with | true => a :: match decide (P b) with | true => b :: List.takeWhile (fun b => decide (P b)) l | false => [] | false => []).eraseIdx (n + 1) I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPa:P a⊢ List.takeWhile (fun b => decide (P b)) ((b :: l).eraseIdx n) = (match decide (P b) with | true => b :: List.takeWhile (fun b => decide (P b)) l | false => []).eraseIdx n exact takeWhile_eraseIdx P (b :: l) n fun i j hij hP => I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPa:P ai:Fin (b :: l).lengthj:Fin (b :: l).lengthhij:i < jhP:P ((b :: l).get j)⊢ P ((b :: l).get i) simpa using h i.succ j.succ (I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPa:P ai:Fin (b :: l).lengthj:Fin (b :: l).lengthhij:i < jhP:P ((b :: l).get j)⊢ i.succ < j.succ All goals completed! 🐙) (I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPa:P ai:Fin (b :: l).lengthj:Fin (b :: l).lengthhij:i < jhP:P ((b :: l).get j)⊢ P ((a :: b :: l).get j.succ) All goals completed! 🐙) I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPa:¬P a⊢ List.takeWhile (fun b => decide (P b)) (a :: (b :: l).eraseIdx n) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx (n + 1) All goals completed! 🐙I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPb:¬P bhPa:P a⊢ (match decide (P a) with | true => if (List.takeWhile (fun b => decide (P b)) (b :: l)).length ≤ n then (List.dropWhile (fun b => decide (P b)) (b :: l)).eraseIdx (n - (List.takeWhile (fun b => decide (P b)) (b :: l)).length) else List.dropWhile (fun b => decide (P b)) (b :: l) | false => a :: (b :: l).eraseIdx n) = if (match decide (P a) with | true => [a] | false => []).length ≤ n + 1 then (match decide (P a) with | true => b :: l | false => a :: b :: l).eraseIdx (n + 1 - (match decide (P a) with | true => [a] | false => []).length) else match decide (P a) with | true => b :: l | false => a :: b :: l All goals completed! 🐙 I:TypeP:I → Propinst✝:DecidablePred Pa:Ib:Il:List In:ℕh:∀ (i j : Fin (a :: b :: l).length), i < j → P ((a :: b :: l).get j) → P ((a :: b :: l).get i)hPb:¬P bhPa:¬P a⊢ (match decide (P a) with | true => List.dropWhile (fun b => decide (P b)) ((b :: l).eraseIdx n) | false => a :: (b :: l).eraseIdx n) = if (match decide (P a) with | true => [a] | false => []).length ≤ n + 1 then (match decide (P a) with | true => b :: l | false => a :: b :: l).eraseIdx (n + 1 - (match decide (P a) with | true => [a] | false => []).length) else match decide (P a) with | true => b :: l | false => a :: b :: l All goals completed! 🐙lemma insertionSort_length {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (l : List I) : (List.insertionSort le1 l).length = l.length := List.length_insertionSort le1 l

The position r0 ends up in r on adding it via List.orderedInsert _ r0 r.

n:ℕI:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ (List.takeWhile (fun b => decide ¬le1 r0 b) r).length < r.length + 1 n:ℕI:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ih1:(List.takeWhile (fun b => decide ¬le1 r0 b) r).length ≤ r.length⊢ (List.takeWhile (fun b => decide ¬le1 r0 b) r).length < r.length + 1 All goals completed! 🐙⟩
lemma orderedInsertPos_lt_length {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : orderedInsertPos le1 r r0 < (r0 :: r).length := I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ ↑(orderedInsertPos le1 r r0) < (r0 :: r).length I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ (List.takeWhile (fun b => decide ¬le1 r0 b) r).length < r.length + 1 All goals completed! 🐙@[simp] lemma orderedInsert_get_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : (List.orderedInsert le1 r0 r)[(orderedInsertPos le1 r r0).val] = r0 := I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ (List.orderedInsert le1 r0 r)[↑(orderedInsertPos le1 r r0)] = r0 All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ List.takeWhile (fun b => decide ¬le1 r0 b) r ++ (r0 :: List.dropWhile (fun b => decide ¬le1 r0 b) r).eraseIdx (↑(orderedInsertPos le1 r r0) - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length) = rI:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ (List.takeWhile (fun b => decide ¬le1 r0 b) r).length ≤ ↑(orderedInsertPos le1 r r0) I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ List.takeWhile (fun b => decide ¬le1 r0 b) r ++ (r0 :: List.dropWhile (fun b => decide ¬le1 r0 b) r).eraseIdx (↑(orderedInsertPos le1 r r0) - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length) = r All goals completed! 🐙 I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ (List.takeWhile (fun b => decide ¬le1 r0 b) r).length ≤ ↑(orderedInsertPos le1 r r0) All goals completed! 🐙lemma orderedInsertPos_cons {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 r1 : I) : (orderedInsertPos le1 (r1 ::r) r0).val = if le1 r0 r1 then ⟨0, n:ℕI:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ir1:I⊢ 0 < (List.orderedInsert le1 r0 r).length + 1 All goals completed! 🐙⟩ else (Fin.succ (orderedInsertPos le1 r r0)) := I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ir1:I⊢ ↑(orderedInsertPos le1 (r1 :: r) r0) = ↑(if le1 r0 r1 then ⟨0, ⋯⟩ else (orderedInsertPos le1 r r0).succ) I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ir1:I⊢ (match !decide (le1 r0 r1) with | true => r1 :: List.takeWhile (fun b => !decide (le1 r0 b)) r | false => []).length = ↑(if le1 r0 r1 then 0 else ⟨(List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1, ⋯⟩) I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ir1:Ih:le1 r0 r1⊢ (match !decide (le1 r0 r1) with | true => r1 :: List.takeWhile (fun b => !decide (le1 r0 b)) r | false => []).length = ↑(if le1 r0 r1 then 0 else ⟨(List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1, ⋯⟩)I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ir1:Ih:¬le1 r0 r1⊢ (match !decide (le1 r0 r1) with | true => r1 :: List.takeWhile (fun b => !decide (le1 r0 b)) r | false => []).length = ↑(if le1 r0 r1 then 0 else ⟨(List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1, ⋯⟩) I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ir1:Ih:le1 r0 r1⊢ (match !decide (le1 r0 r1) with | true => r1 :: List.takeWhile (fun b => !decide (le1 r0 b)) r | false => []).length = ↑(if le1 r0 r1 then 0 else ⟨(List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1, ⋯⟩)I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ir1:Ih:¬le1 r0 r1⊢ (match !decide (le1 r0 r1) with | true => r1 :: List.takeWhile (fun b => !decide (le1 r0 b)) r | false => []).length = ↑(if le1 r0 r1 then 0 else ⟨(List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1, ⋯⟩) All goals completed! 🐙lemma orderedInsertPos_sigma {I : Type} {f : I → Type} (le1 : I → I → Prop) [DecidableRel le1] (l : List (Σ i, f i)) (k : I) (a : f k) : (orderedInsertPos (fun (i j : Σ i, f i) => le1 i.1 j.1) l ⟨k, a⟩).1 = (orderedInsertPos le1 (List.map (fun (i : Σ i, f i) => i.1) l) k).1 := I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1l:List ((i : I) × f i)k:Ia:f k⊢ ↑(orderedInsertPos (fun i j => le1 i.fst j.fst) l ⟨k, a⟩) = ↑(orderedInsertPos le1 (List.map (fun i => i.fst) l) k) I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1l:List ((i : I) × f i)k:Ia:f k⊢ (List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).length induction l with I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1k:Ia:f k⊢ (List.takeWhile (fun b => !decide (le1 k b.fst)) []).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) [])).length All goals completed! 🐙 I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1k:Ia✝:f ka:(i : I) × f il:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).length⊢ (List.takeWhile (fun b => !decide (le1 k b.fst)) (a :: l)).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (a :: l))).length I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1k:Ia✝:f ka:(i : I) × f il:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).length⊢ (match !decide (le1 k a.fst) with | true => a :: List.takeWhile (fun b => !decide (le1 k b.fst)) l | false => []).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (a :: l))).length I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1k:Ia:f kl:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).lengthfst:Isnd:f fst⊢ (match !decide (le1 k ⟨fst, snd⟩.fst) with | true => ⟨fst, snd⟩ :: List.takeWhile (fun b => !decide (le1 k b.fst)) l | false => []).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (⟨fst, snd⟩ :: l))).length I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1k:Ia:f kl:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).lengthfst:Isnd:f fst⊢ (match !decide (le1 k fst) with | true => ⟨fst, snd⟩ :: List.takeWhile (fun b => !decide (le1 k b.fst)) l | false => []).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (⟨fst, snd⟩ :: l))).length I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1k:Ia:f kl:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).lengthfst:Isnd:f fstx✝:Boolheq✝:(!decide (le1 k fst)) = true⊢ (⟨fst, snd⟩ :: List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (⟨fst, snd⟩ :: l))).lengthI:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1k:Ia:f kl:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).lengthfst:Isnd:f fstx✝:Boolheq✝:(!decide (le1 k fst)) = false⊢ [].length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (⟨fst, snd⟩ :: l))).length I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1k:Ia:f kl:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).lengthfst:Isnd:f fstx✝:Boolheq✝:(!decide (le1 k fst)) = true⊢ (⟨fst, snd⟩ :: List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (⟨fst, snd⟩ :: l))).lengthI:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1k:Ia:f kl:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).lengthfst:Isnd:f fstx✝:Boolheq✝:(!decide (le1 k fst)) = false⊢ [].length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (⟨fst, snd⟩ :: l))).length All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ii:ℕhi✝:i < ↑(orderedInsertPos le1 r r0)hi:i < (List.takeWhile (fun b => !decide (le1 r0 b)) r).length⊢ List.takeWhile (fun b => !decide (le1 r0 b)) r <+: r All goals completed! 🐙lemma orderedInsertPos_take_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : (List.take (orderedInsertPos le1 r r0) (List.orderedInsert le1 r0 r)) = List.takeWhile (fun b => decide ¬le1 r0 b) r := I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ List.take (↑(orderedInsertPos le1 r r0)) (List.orderedInsert le1 r0 r) = List.takeWhile (fun b => decide ¬le1 r0 b) r All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In:ℕh1:n < (List.take (↑(orderedInsertPos le1 r r0)) r).lengthh2:n < (List.take (↑(orderedInsertPos le1 r r0)) (List.orderedInsert le1 r0 r)).length⊢ r[n] = r.get ⟨n, ⋯⟩I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In:ℕh1:n < (List.take (↑(orderedInsertPos le1 r r0)) r).lengthh2:n < (List.take (↑(orderedInsertPos le1 r r0)) (List.orderedInsert le1 r0 r)).length⊢ n < ↑(orderedInsertPos le1 r r0) I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In:ℕh1:n < (List.take (↑(orderedInsertPos le1 r r0)) r).lengthh2:n < (List.take (↑(orderedInsertPos le1 r r0)) (List.orderedInsert le1 r0 r)).length⊢ n < ↑(orderedInsertPos le1 r r0) I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In:ℕh2:n < (List.take (↑(orderedInsertPos le1 r r0)) (List.orderedInsert le1 r0 r)).lengthh1:n < ↑(orderedInsertPos le1 r r0) ∧ n < r.length⊢ n < ↑(orderedInsertPos le1 r r0) All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ihr:r = List.takeWhile (fun b => !decide (le1 r0 b)) r ++ List.dropWhile (fun b => !decide (le1 r0 b)) r⊢ List.drop (↑(orderedInsertPos le1 r r0)) (List.takeWhile (fun b => !decide (le1 r0 b)) r) ++ List.drop (↑(orderedInsertPos le1 r r0) - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length) (List.dropWhile (fun b => !decide (le1 r0 b)) r) = List.dropWhile (fun b => !decide (le1 r0 b)) r All goals completed! 🐙All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ List.drop (↑(orderedInsertPos le1 r r0).succ) (List.orderedInsert le1 r0 r) = List.dropWhile (fun b => decide ¬le1 r0 b) r All goals completed! 🐙lemma orderedInsertPos_succ_take_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : (List.take (orderedInsertPos le1 r r0).succ (List.orderedInsert le1 r0 r)) = List.takeWhile (fun b => decide ¬le1 r0 b) r ++ [r0] := I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ List.take (↑(orderedInsertPos le1 r r0).succ) (List.orderedInsert le1 r0 r) = List.takeWhile (fun b => decide ¬le1 r0 b) r ++ [r0] All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r0:Ir:List In:Fin r.lengthhn:↑n < ↑(orderedInsertPos le1 r r0)htake:r.get n ∈ List.takeWhile (fun b => decide ¬le1 r0 b) r⊢ ¬le1 r0 (r.get n) All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r0:Ir:List In:Fin (List.orderedInsert le1 r0 r).lengthhn:n < orderedInsertPos le1 r r0htake:(List.orderedInsert le1 r0 r).get n ∈ List.takeWhile (fun b => decide ¬le1 r0 b) r⊢ ¬le1 r0 ((List.orderedInsert le1 r0 r).get n) All goals completed! 🐙I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1r0:Ir:List Ihs:List.Pairwise le1 rn:Fin r.lengthhn✝:¬↑n < ↑(orderedInsertPos le1 r r0)hn:↑n - ↑(orderedInsertPos le1 r r0) + ↑(orderedInsertPos le1 r r0) < r.length⊢ ∃ (hm : ↑n - ↑(orderedInsertPos le1 r r0) + ↑(orderedInsertPos le1 r r0) < r.length), r[↑(orderedInsertPos le1 r r0) + (↑n - ↑(orderedInsertPos le1 r r0))] = r.get n I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1r0:Ir:List Ihs:List.Pairwise le1 rn:Fin r.lengthhn✝:¬↑n < ↑(orderedInsertPos le1 r r0)hn:↑n - ↑(orderedInsertPos le1 r r0) + ↑(orderedInsertPos le1 r r0) < r.length⊢ r[↑(orderedInsertPos le1 r r0) + (↑n - ↑(orderedInsertPos le1 r r0))] = r.get n I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1r0:Ir:List Ihs:List.Pairwise le1 rn:Fin r.lengthhn✝:¬↑n < ↑(orderedInsertPos le1 r r0)hn:↑n - ↑(orderedInsertPos le1 r r0) + ↑(orderedInsertPos le1 r r0) < r.length⊢ ↑(orderedInsertPos le1 r r0) + (↑n - ↑(orderedInsertPos le1 r r0)) = ↑n All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ii:ℕhr:∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)hi:i < (List.takeWhile (fun b => !decide (le1 r0 b)) r).lengthhi':¬(List.takeWhile (fun b => !decide (le1 r0 b)) r).length ≤ i⊢ r0 :: List.dropWhile (fun b => decide ¬le1 r0 b) r = r0 :: if (List.takeWhile (fun b => decide ¬le1 r0 b) r).length ≤ i then (List.dropWhile (fun b => decide ¬le1 r0 b) r).eraseIdx (i - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length) else List.dropWhile (fun b => decide ¬le1 r0 b) rI:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ii:ℕhi:i < ↑(orderedInsertPos le1 r r0)hr:∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)⊢ ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i) I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ii:ℕhi:i < ↑(orderedInsertPos le1 r r0)hr:∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)⊢ ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i) All goals completed! 🐙 I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ii:ℕhi:i < ↑(orderedInsertPos le1 r r0)hr:∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)⊢ i < (List.takeWhile (fun b => decide ¬le1 r0 b) r).length All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ii:ℕhi:↑⟨(List.takeWhile (fun b => decide ¬le1 r0 b) r).length, ⋯⟩ ≤ ihr:∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)hn:i + 1 - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length = i - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length + 1⊢ (List.takeWhile (fun b => decide ¬le1 r0 b) r).length ≤ i All goals completed! 🐙 I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ii:ℕhi:↑(orderedInsertPos le1 r r0) ≤ ihr:∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)hn:i + 1 - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length = i - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length + 1⊢ ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i) All goals completed! 🐙 I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ii:ℕhi:↑(orderedInsertPos le1 r r0) ≤ ihr:∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)⊢ (List.takeWhile (fun b => decide ¬le1 r0 b) r).length ≤ i.succ I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ii:ℕhi:(List.takeWhile (fun b => decide ¬le1 r0 b) r).length ≤ ihr:∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)⊢ (List.takeWhile (fun b => decide ¬le1 r0 b) r).length ≤ i.succ All goals completed! 🐙

The equivalence between Fin (r0 :: r).length and Fin (List.orderedInsert le1 r0 r).length according to where the elements map, i.e. 0 is taken to orderedInsertPos le1 r r0.

@[`@[expose]` has no effect outside a `module` fileexpose] def orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : Fin (r.length + 1) ≃ Fin (List.orderedInsert le1 r0 r).length := n:ℕI:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ Fin (r.length + 1) ≃ Fin (List.orderedInsert le1 r0 r).length n:ℕI:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ie2:Fin (List.orderedInsert le1 r0 r).length ≃ Fin (r0 :: r).length := (Fin.castOrderIso ⋯).toEquiv⊢ Fin (r.length + 1) ≃ Fin (List.orderedInsert le1 r0 r).length n:ℕI:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ie2:Fin (List.orderedInsert le1 r0 r).length ≃ Fin (r0 :: r).length := (Fin.castOrderIso ⋯).toEquive3:Fin (r0 :: r).length ≃ Fin 1 ⊕ Fin r.length := finExtractOne 0⊢ Fin (r.length + 1) ≃ Fin (List.orderedInsert le1 r0 r).length n:ℕI:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ie2:Fin (List.orderedInsert le1 r0 r).length ≃ Fin (r0 :: r).length := (Fin.castOrderIso ⋯).toEquive3:Fin (r0 :: r).length ≃ Fin 1 ⊕ Fin r.length := finExtractOne 0e4:Fin (r0 :: r).length ≃ Fin 1 ⊕ Fin r.length := finExtractOne ⟨↑(orderedInsertPos le1 r r0), ⋯⟩⊢ Fin (r.length + 1) ≃ Fin (List.orderedInsert le1 r0 r).length All goals completed! 🐙
@[simp] lemma orderedInsertEquiv_zero {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : orderedInsertEquiv le1 r r0 0 = orderedInsertPos le1 r r0 := I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ (orderedInsertEquiv le1 r r0) 0 = orderedInsertPos le1 r r0 All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r✝:List Ir0:In:ℕr1:Ir:List Ihn:n.succ < (r0 :: r1 :: r).length⊢ (Fin.castOrderIso ⋯).symm ((finExtractOne ⟨↑(orderedInsertPos le1 (r1 :: r) r0), ⋯⟩).symm (Sum.inr (predAboveI 0 ⟨n + 1, hn⟩))) = Fin.cast ⋯ (⟨↑(orderedInsertPos le1 (r1 :: r) r0), ⋯⟩.succAbove ⟨n, ⋯⟩)I:Typele1:I → I → Propinst✝:DecidableRel le1r✝:List Ir0:In:ℕr1:Ir:List Ihn:n.succ < (r0 :: r1 :: r).length⊢ 0 ≠ ⟨n + 1, hn⟩ I:Typele1:I → I → Propinst✝:DecidableRel le1r✝:List Ir0:In:ℕr1:Ir:List Ihn:n.succ < (r0 :: r1 :: r).length⊢ (Fin.castOrderIso ⋯).symm (⟨(List.takeWhile (fun b => !decide (le1 r0 b)) (r1 :: r)).length, ⋯⟩.succAbove (predAboveI 0 ⟨n + 1, hn⟩)) = Fin.cast ⋯ (⟨(List.takeWhile (fun b => !decide (le1 r0 b)) (r1 :: r)).length, ⋯⟩.succAbove ⟨n, ⋯⟩)I:Typele1:I → I → Propinst✝:DecidableRel le1r✝:List Ir0:In:ℕr1:Ir:List Ihn:n.succ < (r0 :: r1 :: r).length⊢ 0 ≠ ⟨n + 1, hn⟩ I:Typele1:I → I → Propinst✝:DecidableRel le1r✝:List Ir0:In:ℕr1:Ir:List Ihn:n.succ < (r0 :: r1 :: r).length⊢ 0 ≠ ⟨n + 1, hn⟩ All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r✝:List Ir0:Ir1:Ir:List In:Fin (r1 :: r).length⊢ (Fin.castOrderIso ⋯).symm ((finExtractOne ⟨↑(orderedInsertPos le1 (r1 :: r) r0), ⋯⟩).symm (Sum.inr (predAboveI 0 n.succ))) = Fin.cast ⋯ (⟨↑(orderedInsertPos le1 (r1 :: r) r0), ⋯⟩.succAbove n)I:Typele1:I → I → Propinst✝:DecidableRel le1r✝:List Ir0:Ir1:Ir:List In:Fin (r1 :: r).length⊢ 0 ≠ n.succ I:Typele1:I → I → Propinst✝:DecidableRel le1r✝:List Ir0:Ir1:Ir:List In:Fin (r1 :: r).length⊢ (Fin.castOrderIso ⋯).symm (⟨(List.takeWhile (fun b => !decide (le1 r0 b)) (r1 :: r)).length, ⋯⟩.succAbove (predAboveI 0 n.succ)) = Fin.cast ⋯ (⟨(List.takeWhile (fun b => !decide (le1 r0 b)) (r1 :: r)).length, ⋯⟩.succAbove n)I:Typele1:I → I → Propinst✝:DecidableRel le1r✝:List Ir0:Ir1:Ir:List In:Fin (r1 :: r).length⊢ 0 ≠ n.succ I:Typele1:I → I → Propinst✝:DecidableRel le1r✝:List Ir0:Ir1:Ir:List In:Fin (r1 :: r).length⊢ 0 ≠ n.succ All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In:Fin r.lengthm:Fin r.lengthhx:↑(Fin.cast ⋯ (⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove ⟨↑n, ⋯⟩)) < ↑(Fin.cast ⋯ (⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove ⟨↑m, ⋯⟩))⊢ n < m I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In:Fin r.lengthm:Fin r.lengthhx:⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove n < ⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove m⊢ n < m rwa [I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In:Fin r.lengthm:Fin r.lengthhx:n < m⊢ n < mI:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In:Fin r.lengthm:Fin r.lengthhx:n < m⊢ n < m at hxlemma orderedInsertEquiv_congr {α : Type} {r : α → α → Prop} [DecidableRel r] (a : α) (l l' : List α) (h : l = l') : orderedInsertEquiv r l a = (Fin.castOrderIso (n:ℕα:Typer:α → α → Propinst✝:DecidableRel ra:αl:List αl':List αh:l = l'⊢ l.length + 1 = l'.length + 1 All goals completed! 🐙)).toEquiv.trans ((orderedInsertEquiv r l' a).trans (Fin.castOrderIso (n:ℕα:Typer:α → α → Propinst✝:DecidableRel ra:αl:List αl':List αh:l = l'⊢ (List.orderedInsert r a l').length = (List.orderedInsert r a l).length All goals completed! 🐙)).toEquiv) := α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List αl':List αh:l = l'⊢ orderedInsertEquiv r l a = (Fin.castOrderIso ⋯).trans ((orderedInsertEquiv r l' a).trans (Fin.castOrderIso ⋯).toEquiv) α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List α⊢ orderedInsertEquiv r l a = (Fin.castOrderIso ⋯).trans ((orderedInsertEquiv r l a).trans (Fin.castOrderIso ⋯).toEquiv) All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ix:Fin (r0 :: r).lengthn:ℕh:n.succ < (r0 :: r).lengthhn:¬n < ↑(orderedInsertPos le1 r r0)hn':¬n + 1 < (List.takeWhile (fun b => !decide (le1 r0 b)) r).lengthhnn:n + 1 - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length = n - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1hr:r.length = (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + (List.dropWhile (fun b => !decide (le1 r0 b)) r).length⊢ n = r.length - (List.dropWhile (fun b => !decide (le1 r0 b)) r).length + (n - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length) I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ix:Fin (r0 :: r).lengthn:ℕh:n.succ < (r0 :: r).lengthhn:¬n < ↑(orderedInsertPos le1 r r0)hn':¬n + 1 < (List.takeWhile (fun b => !decide (le1 r0 b)) r).lengthhnn:n + 1 - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length = n - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1hr:r.length = (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + (List.dropWhile (fun b => !decide (le1 r0 b)) r).length⊢ n = (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + (n - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length) All goals completed! 🐙lemma orderedInsertEquiv_get {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : (r0 :: r).get ∘ (orderedInsertEquiv le1 r r0).symm = (List.orderedInsert le1 r0 r).get := I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ (r0 :: r).get ∘ ⇑(orderedInsertEquiv le1 r r0).symm = (List.orderedInsert le1 r0 r).get I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:Ix:Fin (List.orderedInsert le1 r0 r).length⊢ ((r0 :: r).get ∘ ⇑(orderedInsertEquiv le1 r r0).symm) x = (List.orderedInsert le1 r0 r).get x All goals completed! 🐙lemma orderedInsert_eraseIdx_orderedInsertEquiv_zero {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : (List.orderedInsert le1 r0 r).eraseIdx (orderedInsertEquiv le1 r r0 ⟨0, n:ℕI:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ 0 < r.length + 1 All goals completed! 🐙⟩) = r := I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:I⊢ (List.orderedInsert le1 r0 r).eraseIdx ↑((orderedInsertEquiv le1 r r0) ⟨0, ⋯⟩) = r All goals completed! 🐙I:Typele1:I → I → Propinst✝:DecidableRel le1r0:In:ℕr1:Ir:List Iih:∀ (hn : n.succ < (r0 :: r).length), (∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)) → (List.orderedInsert le1 r0 r).eraseIdx ↑((orderedInsertEquiv le1 r r0) ⟨n.succ, hn⟩) = List.orderedInsert le1 r0 (r.eraseIdx n)hn:n.succ < (r0 :: r1 :: r).lengthhr:∀ (i j : Fin (r1 :: r).length), i < j → ¬le1 r0 ((r1 :: r).get j) → ¬le1 r0 ((r1 :: r).get i)hn':¬n < ↑(orderedInsertPos le1 (r1 :: r) r0)⊢ ↑(orderedInsertPos le1 (r1 :: r) r0) ≤ n All goals completed! 🐙lemma orderedInsert_eraseIdx_orderedInsertEquiv_fin_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (n : Fin r.length) (hr : ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)) : (List.orderedInsert le1 r0 r).eraseIdx (orderedInsertEquiv le1 r r0 n.succ) = (List.orderedInsert le1 r0 (r.eraseIdx n)) := I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In:Fin r.lengthhr:∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)⊢ (List.orderedInsert le1 r0 r).eraseIdx ↑((orderedInsertEquiv le1 r r0) n.succ) = List.orderedInsert le1 r0 (r.eraseIdx ↑n) All goals completed! 🐙I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1l:List ((i : I) × f i)i:Ia:f ix:Fin (l.length + 1)n:ℕh0:n.succ < l.length + 1⊢ ↑(if ⟨n, ⋯⟩.castSucc < ⟨↑(orderedInsertPos le1 (List.map (fun i => i.fst) l) i), ⋯⟩ then ⟨n, ⋯⟩.castSucc else ⟨n, ⋯⟩.succ) = ↑(if ⟨n, ⋯⟩.castSucc < ⟨↑(orderedInsertPos le1 (List.map (fun i => i.fst) l) i), ⋯⟩ then ⟨n, ⋯⟩.castSucc else ⟨n, ⋯⟩.succ) I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1l:List ((i : I) × f i)i:Ia:f ix:Fin (l.length + 1)n:ℕh0:n.succ < l.length + 1⊢ ↑(if n < ↑(orderedInsertPos le1 (List.map (fun i => i.fst) l) i) then ⟨n, ⋯⟩ else ⟨n + 1, ⋯⟩) = ↑(if n < ↑(orderedInsertPos le1 (List.map (fun i => i.fst) l) i) then ⟨n, ⋯⟩ else ⟨n + 1, ⋯⟩) I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1l:List ((i : I) × f i)i:Ia:f ix:Fin (l.length + 1)n:ℕh0:n.succ < l.length + 1h✝:n < ↑(orderedInsertPos le1 (List.map (fun i => i.fst) l) i)⊢ ↑⟨n, ⋯⟩ = ↑⟨n, ⋯⟩I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1l:List ((i : I) × f i)i:Ia:f ix:Fin (l.length + 1)n:ℕh0:n.succ < l.length + 1h✝:¬n < ↑(orderedInsertPos le1 (List.map (fun i => i.fst) l) i)⊢ ↑⟨n + 1, ⋯⟩ = ↑⟨n + 1, ⋯⟩ I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1l:List ((i : I) × f i)i:Ia:f ix:Fin (l.length + 1)n:ℕh0:n.succ < l.length + 1h✝:n < ↑(orderedInsertPos le1 (List.map (fun i => i.fst) l) i)⊢ ↑⟨n, ⋯⟩ = ↑⟨n, ⋯⟩I:Typef:I → Typele1:I → I → Propinst✝:DecidableRel le1l:List ((i : I) × f i)i:Ia:f ix:Fin (l.length + 1)n:ℕh0:n.succ < l.length + 1h✝:¬n < ↑(orderedInsertPos le1 (List.map (fun i => i.fst) l) i)⊢ ↑⟨n + 1, ⋯⟩ = ↑⟨n + 1, ⋯⟩ All goals completed! 🐙set_option maxHeartbeats 350000I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In'✝:Fin (r.length + 1)n':ℕh0:n'.succ < r.length + 1h1:↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩) < (List.orderedInsert le1 r0 r).lengthh2:↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩) < (r.insertIdx (↑(orderedInsertPos le1 r r0)) r0).lengthhn'✝:(orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩ = ⟨↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩), h1⟩hr:↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩) = ↑(Fin.cast ⋯ (⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove ⟨n', ⋯⟩))hx:⟨↑((orderedInsertEquiv le1 r r0) ⟨n' + 1, h0⟩), h2⟩ = ⟨↑(⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove ⟨n', ⋯⟩), ⋯⟩hn':¬n' < ↑(orderedInsertPos le1 r r0)⊢ r[n'] = r[n' + 1 - 1]I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In'✝:Fin (r.length + 1)n':ℕh0:n'.succ < r.length + 1h1:↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩) < (List.orderedInsert le1 r0 r).lengthh2:↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩) < (r.insertIdx (↑(orderedInsertPos le1 r r0)) r0).lengthhn'✝:(orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩ = ⟨↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩), h1⟩hr:↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩) = ↑(Fin.cast ⋯ (⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove ⟨n', ⋯⟩))hx:⟨↑((orderedInsertEquiv le1 r r0) ⟨n' + 1, h0⟩), h2⟩ = ⟨↑(⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove ⟨n', ⋯⟩), ⋯⟩hn':¬n' < ↑(orderedInsertPos le1 r r0)⊢ ↑(orderedInsertPos le1 r r0) < n' + 1 I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In'✝:Fin (r.length + 1)n':ℕh0:n'.succ < r.length + 1h1:↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩) < (List.orderedInsert le1 r0 r).lengthh2:↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩) < (r.insertIdx (↑(orderedInsertPos le1 r r0)) r0).lengthhn'✝:(orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩ = ⟨↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩), h1⟩hr:↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩) = ↑(Fin.cast ⋯ (⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove ⟨n', ⋯⟩))hx:⟨↑((orderedInsertEquiv le1 r r0) ⟨n' + 1, h0⟩), h2⟩ = ⟨↑(⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove ⟨n', ⋯⟩), ⋯⟩hn':¬n' < ↑(orderedInsertPos le1 r r0)⊢ r[n'] = r[n' + 1 - 1] All goals completed! 🐙 I:Typele1:I → I → Propinst✝:DecidableRel le1r:List Ir0:In'✝:Fin (r.length + 1)n':ℕh0:n'.succ < r.length + 1h1:↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩) < (List.orderedInsert le1 r0 r).lengthh2:↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩) < (r.insertIdx (↑(orderedInsertPos le1 r r0)) r0).lengthhn'✝:(orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩ = ⟨↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩), h1⟩hr:↑((orderedInsertEquiv le1 r r0) ⟨n'.succ, h0⟩) = ↑(Fin.cast ⋯ (⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove ⟨n', ⋯⟩))hx:⟨↑((orderedInsertEquiv le1 r r0) ⟨n' + 1, h0⟩), h2⟩ = ⟨↑(⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove ⟨n', ⋯⟩), ⋯⟩hn':¬n' < ↑(orderedInsertPos le1 r r0)⊢ ↑(orderedInsertPos le1 r r0) < n' + 1 All goals completed! 🐙

The equivalence between Fin l.length ≃ Fin (List.insertionSort r l).length induced by the sorting algorithm.

def insertionSortEquiv {α : Type} (r : α → α → Prop) [DecidableRel r] : (l : List α) → Fin l.length ≃ Fin (List.insertionSort r l).length | [] => Equiv.refl _ | a :: l => (Fin.equivCons (insertionSortEquiv r l)).trans (orderedInsertEquiv r (List.insertionSort r l) a)
α:Typer:α → α → Propinst✝:DecidableRel ra:αl:List αhl:(a :: l).get ∘ ⇑(equivCons (insertionSortEquiv r l)).symm = (a :: List.insertionSort r l).get⊢ (List.orderedInsert r a (List.insertionSort r l)).get = (List.insertionSort r (a :: l)).get All goals completed! 🐙lemma insertionSortEquiv_congr {α : Type} {r : α → α → Prop} [DecidableRel r] (l l' : List α) (h : l = l') : insertionSortEquiv r l = (Fin.castOrderIso (n:ℕα:Typer:α → α → Propinst✝:DecidableRel rl:List αl':List αh:l = l'⊢ l.length = l'.length All goals completed! 🐙)).toEquiv.trans ((insertionSortEquiv r l').trans (Fin.castOrderIso (n:ℕα:Typer:α → α → Propinst✝:DecidableRel rl:List αl':List αh:l = l'⊢ (List.insertionSort r l').length = (List.insertionSort r l).length All goals completed! 🐙)).toEquiv) := α:Typer:α → α → Propinst✝:DecidableRel rl:List αl':List αh:l = l'⊢ insertionSortEquiv r l = (Fin.castOrderIso ⋯).trans ((insertionSortEquiv r l').trans (Fin.castOrderIso ⋯).toEquiv) α:Typer:α → α → Propinst✝:DecidableRel rl:List α⊢ insertionSortEquiv r l = (Fin.castOrderIso ⋯).trans ((insertionSortEquiv r l).trans (Fin.castOrderIso ⋯).toEquiv) All goals completed! 🐙α:Typer:α → α → Propinst✝:DecidableRel rl:List αl':List αh:l = l'i:Fin l.length⊢ ((Fin.castOrderIso ⋯).trans ((insertionSortEquiv r l').trans (Fin.castOrderIso ⋯).toEquiv)) i = Fin.cast ⋯ ((insertionSortEquiv r l') (Fin.cast ⋯ i)) All goals completed! 🐙lemma insertionSort_get_comp_insertionSortEquiv {α : Type} {r : α → α → Prop} [DecidableRel r] (l : List α) : (List.insertionSort r l).get ∘ (insertionSortEquiv r l) = l.get := α:Typer:α → α → Propinst✝:DecidableRel rl:List α⊢ (List.insertionSort r l).get ∘ ⇑(insertionSortEquiv r l) = l.get α:Typer:α → α → Propinst✝:DecidableRel rl:List αx:Fin l.length⊢ ((List.insertionSort r l).get ∘ ⇑(insertionSortEquiv r l)) x = l.get x All goals completed! 🐙All goals completed! 🐙α:Typer:α → α → Propinst✝:DecidableRel ra:αas:List αhi:0 < (a :: as).lengthj:ℕhj:j + 1 < (a :: as).lengthhij:⟨0, hi⟩ < ⟨j + 1, hj⟩hij':(insertionSortEquiv r (a :: as)) ⟨j + 1, hj⟩ < (orderedInsertEquiv r (List.insertionSort r as) a) 0⊢ as[j] = ((a :: as).get ∘ ⇑(insertionSortEquiv r (a :: as)).symm) ((insertionSortEquiv r (a :: as)) ⟨j + 1, hj⟩) All goals completed! 🐙 α:Typer:α → α → Propinst✝:DecidableRel ra:αas:List αi:ℕhi:i + 1 < (a :: as).lengthj:ℕhj:j + 1 < (a :: as).lengthhij:⟨i + 1, hi⟩ < ⟨j + 1, hj⟩hij':(insertionSortEquiv r (a :: as)) ⟨j + 1, hj⟩ < (insertionSortEquiv r (a :: as)) ⟨i + 1, hi⟩⊢ ¬r (a :: as)[⟨i + 1, hi⟩] (a :: as)[⟨j + 1, hj⟩] α:Typer:α → α → Propinst✝:DecidableRel ra:αas:List αi:ℕhi:i + 1 < (a :: as).lengthj:ℕhj:j + 1 < (a :: as).lengthhij:⟨i + 1, hi⟩ < ⟨j + 1, hj⟩hij':(insertionSortEquiv r (a :: as)) ⟨j + 1, hj⟩ < (insertionSortEquiv r (a :: as)) ⟨i + 1, hi⟩⊢ ¬r (a :: as)[⟨i + 1, hi⟩] (a :: as)[⟨j + 1, hj⟩] α:Typer:α → α → Propinst✝:DecidableRel ra:αas:List αi:ℕhi:i + 1 < (a :: as).lengthj:ℕhj:j + 1 < (a :: as).lengthhij:⟨i + 1, hi⟩ < ⟨j + 1, hj⟩hij':(orderedInsertEquiv r (List.insertionSort r as) a) ((insertionSortEquiv r as) ⟨j, ⋯⟩).succ < (orderedInsertEquiv r (List.insertionSort r as) a) ((insertionSortEquiv r as) ⟨i, ⋯⟩).succ⊢ ¬r (a :: as)[⟨i + 1, hi⟩] (a :: as)[⟨j + 1, hj⟩] simpa using insertionSortEquiv_order as ⟨i, Nat.succ_lt_succ_iff.mp hi⟩ ⟨j, Nat.succ_lt_succ_iff.mp hj⟩ (α:Typer:α → α → Propinst✝:DecidableRel ra:αas:List αi:ℕhi:i + 1 < (a :: as).lengthj:ℕhj:j + 1 < (a :: as).lengthhij:⟨i + 1, hi⟩ < ⟨j + 1, hj⟩hij':(orderedInsertEquiv r (List.insertionSort r as) a) ((insertionSortEquiv r as) ⟨j, ⋯⟩).succ < (orderedInsertEquiv r (List.insertionSort r as) a) ((insertionSortEquiv r as) ⟨i, ⋯⟩).succ⊢ ⟨i, ⋯⟩ < ⟨j, ⋯⟩ All goals completed! 🐙) (orderedInsertEquiv_monotone_fin_succ _ _ _ _ _ hij')

Optional erase of an element in a list. For none returns the list, for some i returns the list with the i'th element erased.

@[`@[expose]` has no effect outside a `module` fileexpose] def optionErase {I : Type} (l : List I) (i : Option (Fin l.length)) : List I := match i with | none => l | some i => List.eraseIdx l i
lemma eraseIdx_length' {I : Type} (l : List I) (i : Fin l.length) : (List.eraseIdx l i).length = l.length - 1 := I:Typel:List Ii:Fin l.length⊢ (l.eraseIdx ↑i).length = l.length - 1 All goals completed! 🐙lemma eraseIdx_length {I : Type} (l : List I) (i : Fin l.length) : (List.eraseIdx l i).length + 1 = l.length := List.length_eraseIdx_add_one i.isLtlemma eraseIdx_length_succ {I : Type} (l : List I) (i : Fin l.length) : (List.eraseIdx l i).length.succ = l.length := List.length_eraseIdx_add_one i.isLtlemma eraseIdx_cons_length {I : Type} (a : I) (l : List I) (i : Fin (a :: l).length) : (List.eraseIdx (a :: l) i).length= l.length := I:Typea:Il:List Ii:Fin (a :: l).length⊢ ((a :: l).eraseIdx ↑i).length = l.length All goals completed! 🐙I:Typel:List Ii:Fin l.lengthx:Fin (l.eraseIdx ↑i).lengthhi✝:¬x.castSucc < Fin.cast ⋯ ihi:↑i ≤ ↑xhn:¬↑x < ↑i⊢ (if h' : ↑x < ↑i then l[↑x] else l[↑x + 1]) = l[↑x + 1] All goals completed! 🐙I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:ℕr0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i)) → (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ↑((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) ⟨n, ⋯⟩).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩))⊢ (List.foldr (List.orderedInsert le1) [] (r0 :: r)).eraseIdx ↑((orderedInsertEquiv le1 (List.foldr (List.orderedInsert le1) [] r) r0) ((insertionSortEquiv le1 r) ⟨n, ⋯⟩).succ) = List.foldr (List.orderedInsert le1) [] ((r0 :: r).eraseIdx (n + 1)) erw [I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:ℕr0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i)) → (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ↑((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) ⟨n, ⋯⟩).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩))⊢ List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩)) = List.foldr (List.orderedInsert le1) [] ((r0 :: r).eraseIdx (n + 1))I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:ℕr0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i)) → (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ↑((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) ⟨n, ⋯⟩).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩))⊢ ∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i)I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:ℕr0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i)) → (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ↑((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) ⟨n, ⋯⟩).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩))⊢ List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩)) = List.foldr (List.orderedInsert le1) [] ((r0 :: r).eraseIdx (n + 1))I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:ℕr0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i)) → (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ↑((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) ⟨n, ⋯⟩).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩))⊢ ∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i) I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:ℕr0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i)) → (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ↑((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) ⟨n, ⋯⟩).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩))⊢ (List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩) = List.foldr (List.orderedInsert le1) [] (r.eraseIdx n)I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:ℕr0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i)) → (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ↑((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) ⟨n, ⋯⟩).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩))⊢ ∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i) I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:ℕr0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i)) → (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ↑((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) ⟨n, ⋯⟩).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩))⊢ ∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i) I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:ℕr0:Ir:List Ihn✝:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i)) → (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ↑((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) ⟨n, ⋯⟩).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩))i:Fin (List.insertionSort le1 r).lengthj:Fin (List.insertionSort le1 r).lengthhij:i < jhn:¬le1 r0 ((List.insertionSort le1 r).get j)⊢ ¬le1 r0 ((List.insertionSort le1 r).get i) I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:ℕr0:Ir:List Ihn✝:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i)) → (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ↑((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) ⟨n, ⋯⟩).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩))i:Fin (List.insertionSort le1 r).lengthj:Fin (List.insertionSort le1 r).lengthhij:i < jhn:¬le1 r0 ((List.insertionSort le1 r).get j)hx:le1 ((List.insertionSort le1 r).get i) ((List.insertionSort le1 r).get j)⊢ ¬le1 r0 ((List.insertionSort le1 r).get i) I:Typele1:I → I → Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:ℕr0:Ir:List Ihn✝:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j → ¬le1 r0 ((List.insertionSort le1 r).get j) → ¬le1 r0 ((List.insertionSort le1 r).get i)) → (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ↑((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) ⟨n, ⋯⟩).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, ⋯⟩))i:Fin (List.insertionSort le1 r).lengthj:Fin (List.insertionSort le1 r).lengthhij:i < jhn:¬le1 r0 ((List.insertionSort le1 r).get j)hx:le1 ((List.insertionSort le1 r).get i) ((List.insertionSort le1 r).get j)ht:∀ (i j k : I), le1 i j → ¬le1 k j → ¬le1 k i⊢ ¬le1 r0 ((List.insertionSort le1 r).get i) All goals completed! 🐙lemma eraseIdx_insertionSort_fin {I : Type} (le1 : I → I → Prop) [DecidableRel le1] [Std.Total le1] [IsTrans I le1] (r : List I) (n : Fin r.length) : (List.insertionSort le1 r).eraseIdx ↑((Physlib.List.insertionSortEquiv le1 r) n) = List.insertionSort le1 (r.eraseIdx n) := eraseIdx_insertionSort le1 n.val r (Fin.prop n)

Given a list i :: l the left-most minimal position a of i :: l wrt r. That is the first position of l such that for every element (i :: l)[b] before that position r ((i :: l)[b]) ((i :: l)[a]) is not true. The use of i :: l here rather then just l is to ensure that such a position exists. .

n:ℕα:Typer:α → α → Propinst✝:DecidableRel ri:αl:List α⊢ 0 < (i :: l).length All goals completed! 🐙⟩

The element of i :: l at insertionSortMinPos.

@[`@[expose]` has no effect outside a `module` fileexpose] def insertionSortMin {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) : α := (i :: l).get (insertionSortMinPos r i l)
α:Typer:α → α → Propinst✝:DecidableRel ri:αl:List α⊢ insertionSortMin r i l = ((i :: l).get ∘ ⇑(insertionSortEquiv r (i :: l)).symm) ⟨0, ⋯⟩ All goals completed! 🐙 α:Typer:α → α → Propinst✝:DecidableRel ri:αl:List α⊢ (List.insertionSort r (i :: l)).get ⟨0, ⋯⟩ = (List.insertionSort r (i :: l)).head ⋯ All goals completed! 🐙

The list remaining after dropping the element at the position determined by insertionSortMinPos.

@[`@[expose]` has no effect outside a `module` fileexpose] def insertionSortDropMinPos {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) : List α := (i :: l).eraseIdx (insertionSortMinPos r i l)
α:Typer:α → α → Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ri:αl:List α⊢ List.foldr (List.orderedInsert r) [] (i :: l) = (List.insertionSort r (i :: l)).head ⋯ :: (List.foldr (List.orderedInsert r) [] (i :: l)).tail All goals completed! 🐙

Optional erase of an element in a list, with addition for none. For none adds a to the front of the list, for some i removes the ith element of the list (does not add a). E.g. optionEraseZ [0, 1, 2] 4 none = [4, 0, 1, 2] and optionEraseZ [0, 1, 2] 4 (some 1) = [0, 2].

@[`@[expose]` has no effect outside a `module` fileexpose] def optionEraseZ {I : Type} (l : List I) (a : I) (i : Option (Fin l.length)) : List I := match i with | none => a :: l | some i => List.eraseIdx l i
@[simp] lemma optionEraseZ_some_length {I : Type} (l : List I) (a : I) (i : (Fin l.length)) : (optionEraseZ l a (some i)).length = l.length - 1 := I:Typel:List Ia:Ii:Fin l.length⊢ (optionEraseZ l a (some i)).length = l.length - 1 All goals completed! 🐙All goals completed! 🐙)) i = i') : optionEraseZ l a i = optionEraseZ l' a' i' := I:Typel:List Il':List Ia:Ia':Ii:Option (Fin l.length)i':Option (Fin l'.length)hl:l = l'ha:a = a'hi:Option.map (Fin.cast ⋯) i = i'⊢ optionEraseZ l a i = optionEraseZ l' a' i' I:Typel:List Ia:Ia':Ii:Option (Fin l.length)ha:a = a'i':Option (Fin l.length)hi:Option.map (Fin.cast ⋯) i = i'⊢ optionEraseZ l a i = optionEraseZ l a' i' I:Typel:List Ia:Ii:Option (Fin l.length)i':Option (Fin l.length)hi:Option.map (Fin.cast ⋯) i = i'⊢ optionEraseZ l a i = optionEraseZ l a i' I:Typel:List Ia:Ii:Option (Fin l.length)⊢ optionEraseZ l a i = optionEraseZ l a (Option.map (Fin.cast ⋯) i) I:Typel:List Ia:Ii:Option (Fin l.length)⊢ i = Option.map (Fin.cast ⋯) i All goals completed! 🐙n:ℕm:ℕi:ℕh:i + 1 < n + 1a:Fin nha:↑a < m ∧ ↑a.succ = ↑⟨i + 1, h⟩⊢ i < m n:ℕm:ℕi:ℕh:i + 1 < n + 1a:Fin nha:↑a < m ∧ ↑a = i⊢ i < m All goals completed! 🐙 n:ℕm:ℕi:ℕh:i + 1 < n + 1⊢ i < m → ∃ a ∈ List.take m (List.finRange n), a.succ = ⟨i + 1, h⟩ n:ℕm:ℕi:ℕh:i + 1 < n + 1h1:i < m⊢ ∃ a ∈ List.take m (List.finRange n), a.succ = ⟨i + 1, h✝⟩ n:ℕm:ℕi:ℕh:i + 1 < n + 1h1:i < m⊢ ⟨i, ⋯⟩ ∈ List.take m (List.finRange n) ∧ ⟨i, ⋯⟩.succ = ⟨i + 1, h⟩ n:ℕm:ℕi:ℕh:i + 1 < n + 1h1:i < m⊢ ⟨i, ⋯⟩ ∈ List.take m (List.finRange n) rwa [n:ℕm:ℕi:ℕh:i + 1 < n + 1h1:i < m⊢ ↑⟨i, ⋯⟩ < mn:ℕm:ℕi:ℕh:i + 1 < n + 1h1:i < m⊢ ↑⟨i, ⋯⟩ < m