ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>l₁ : List α<VAR>l₂ : List β<VAR>z : γ<VAR>i : ℕ<GOAL>(List.zipWith f l₁ l₂)[i]? = some z ↔ ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>l₁ : List α<VAR>l₂ : List β<VAR>z : γ<VAR>i : ℕ<GOAL>(List.zipWith f l₁ l₂).get? i = some z ↔ ∃ x y, l₁.get? i = some x ∧ l₂.get? i = some y ∧ f x y = z
<VAR>α : Type u<VAR>β : Type u_1<VAR>l₁ : List α<VAR>l₂ : List β<VAR>z : α × β<VAR>i : ℕ<GOAL>(l₁.zip l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2
<VAR>α : Type u<VAR>β : Type u_1<VAR>l₁ : List α<VAR>l₂ : List β<VAR>z : α × β<VAR>i : ℕ<GOAL>(l₁.zip l₂).get? i = some z ↔ l₁.get? i = some z.1 ∧ l₂.get? i = some z.2
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>l : List α<VAR>l' : List β<VAR>i : ℕ<VAR>h : i < (List.zipWith f l l').length<GOAL>(List.zipWith f l l')[i] = f l[i] l'[i]
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>l : List α<VAR>l' : List β<VAR>i : Fin (List.zipWith f l l').length<GOAL>(List.zipWith f l l').get i = f (l.get ⟨↑i, ⋯⟩) (l'.get ⟨↑i, ⋯⟩)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>l : List α<VAR>l' : List β<VAR>i : ℕ<VAR>h : i < (List.zipWith f l l').length<GOAL>(List.zipWith f l l').nthLe i h = f (l.nthLe i ⋯) (l'.nthLe i ⋯)
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List α<VAR>l' : List β<VAR>i : ℕ<VAR>h : i < (l.zip l').length<GOAL>(l.zip l')[i] = (l[i], l'[i])
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List α<VAR>l' : List β<VAR>i : Fin (l.zip l').length<GOAL>(l.zip l').get i = (l.get ⟨↑i, ⋯⟩, l'.get ⟨↑i, ⋯⟩)
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List α<VAR>l' : List β<VAR>i : ℕ<VAR>h : i < (l.zip l').length<GOAL>(l.zip l').nthLe i h = (l.nthLe i ⋯, l'.nthLe i ⋯)
<VAR>α : Type u<VAR>l init tail : List α<GOAL>(init, tail) ∈ l.inits.zip l.tails ↔ init ++ tail = l
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>l : List α<VAR>l' : List β<GOAL>List.map (Function.uncurry f) (l.zip l') = List.zipWith f l l'
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>l : List α<VAR>l' : List β<VAR>h : l.length = l'.length<GOAL>(List.zipWith f l l').reverse = List.zipWith f l.reverse l'.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S : α → β → Prop<VAR>H : ∀ (a : α) (b : β), R a b → S a b<VAR>l₁ : List α<VAR>l₂ : List β<VAR>h : List.Forall₂ R l₁ l₂<GOAL>List.Forall₂ S l₁ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S Q : α → β → Prop<VAR>h : ∀ (a : α) (b : β), Q a b → R a b → S a b<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.Forall₂ Q l₁ l₂ → List.Forall₂ R l₁ l₂ → List.Forall₂ S l₁ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>a : List α<VAR>b : List β<GOAL>List.Forall₂ (flip R) b a → List.Forall₂ R a b
<VAR>α : Type u_1<VAR>Rₐ : α → α → Prop<VAR>l : List α<GOAL>List.Forall₂ Rₐ l l ↔ ∀ (x : α), x ∈ l → Rₐ x x
<VAR>α : Type u_1<VAR>Rₐ : α → α → Prop<VAR>IsRefl α Rₐ<VAR>l : List α<GOAL>List.Forall₂ Rₐ l l
<VAR>α : Type u_1<GOAL>(List.Forall₂ fun x x_1 => x = x_1) = Eq
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>l : List β<GOAL>List.Forall₂ R [] l ↔ l = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>l : List α<GOAL>List.Forall₂ R l [] ↔ l = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>a : α<VAR>l : List α<VAR>u : List β<GOAL>List.Forall₂ R (a :: l) u ↔ ∃ b u', R a b ∧ List.Forall₂ R l u' ∧ u = b :: u'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>b : β<VAR>l : List β<VAR>u : List α<GOAL>List.Forall₂ R u (b :: l) ↔ ∃ a u', R a b ∧ List.Forall₂ R u' l ∧ u = a :: u'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>p : α → Prop<VAR>l : List α<VAR>u : List β<GOAL>List.Forall₂ (fun a b => p a ∧ R a b) l u ↔ (∀ (a : α), a ∈ l → p a) ∧ List.Forall₂ R l u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>R : α → β → Prop<VAR>f : γ → α<VAR>l : List γ<VAR>u : List β<GOAL>List.Forall₂ R (List.map f l) u ↔ List.Forall₂ (fun c b => R (f c) b) l u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>R : α → β → Prop<VAR>f : γ → β<VAR>l : List α<VAR>u : List γ<GOAL>List.Forall₂ R l (List.map f u) ↔ List.Forall₂ (fun a c => R a (f c)) l u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>hr : Relator.LeftUnique R<VAR>a b : List α<VAR>c : List β<GOAL>List.Forall₂ R a c → List.Forall₂ R b c → a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>hr : Relator.LeftUnique R<GOAL>Relator.LeftUnique (List.Forall₂ R)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>hr : Relator.RightUnique R<VAR>a : List α<VAR>b c : List β<GOAL>List.Forall₂ R a b → List.Forall₂ R a c → b = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>hr : Relator.RightUnique R<GOAL>Relator.RightUnique (List.Forall₂ R)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>hr : Relator.BiUnique R<GOAL>Relator.BiUnique (List.Forall₂ R)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.Forall₂ R l₁ l₂ → l₁.length = l₂.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>x : List α<VAR>y : List β<GOAL>List.Forall₂ R x y → ∀ ⦃i : ℕ⦄ (hx : i < x.length) (hy : i < y.length), R (x.get ⟨i, hx⟩) (y.get ⟨i, hy⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>x : List α<VAR>y : List β<VAR>h : List.Forall₂ R x y<VAR>i : ℕ<VAR>hx : i < x.length<VAR>hy : i < y.length<GOAL>R (x.nthLe i hx) (y.nthLe i hy)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>x : List α<VAR>y : List β<GOAL>x.length = y.length → (∀ (i : ℕ) (h₁ : i < x.length) (h₂ : i < y.length), R (x.get ⟨i, h₁⟩) (y.get ⟨i, h₂⟩)) → List.Forall₂ R x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>x : List α<VAR>y : List β<VAR>H : x.length = y.length<VAR>H' : ∀ (i : ℕ) (h₁ : i < x.length) (h₂ : i < y.length), R (x.nthLe i h₁) (y.nthLe i h₂)<GOAL>List.Forall₂ R x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.Forall₂ R l₁ l₂ ↔ l₁.length = l₂.length ∧ ∀ (i : ℕ) (h₁ : i < l₁.length) (h₂ : i < l₂.length), R (l₁.get ⟨i, h₁⟩) (l₂.get ⟨i, h₂⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.Forall₂ R l₁ l₂ ↔ l₁.length = l₂.length ∧ ∀ (i : ℕ) (h₁ : i < l₁.length) (h₂ : i < l₂.length), R (l₁.nthLe i h₁) (l₂.nthLe i h₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.Forall₂ R l₁ l₂ → ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.Forall₂ R l₁ l₂ ↔ l₁.length = l₂.length ∧ ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>n : ℕ<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.Forall₂ R l₁ l₂ → List.Forall₂ R (List.take n l₁) (List.take n l₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>n : ℕ<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.Forall₂ R l₁ l₂ → List.Forall₂ R (List.drop n l₁) (List.drop n l₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>l : List α<VAR>l₁ l₂ : List β<VAR>h : List.Forall₂ R l (l₁ ++ l₂)<GOAL>List.Forall₂ R (List.take l₁.length l) l₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>l : List α<VAR>l₁ l₂ : List β<VAR>h : List.Forall₂ R l (l₁ ++ l₂)<GOAL>List.Forall₂ R (List.drop l₁.length l) l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>hr : Relator.BiUnique R<GOAL>(R ⇒ List.Forall₂ R ⇒ Iff) (fun x x_1 => x ∈ x_1) fun x x_1 => x ∈ x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R : α → β → Prop<VAR>P : γ → δ → Prop<GOAL>((R ⇒ P) ⇒ List.Forall₂ R ⇒ List.Forall₂ P) List.map List.map
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<GOAL>(List.Forall₂ R ⇒ List.Forall₂ R ⇒ List.Forall₂ R) (fun x x_1 => x ++ x_1) fun x x_1 => x ++ x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<GOAL>(List.Forall₂ R ⇒ List.Forall₂ R) List.reverse List.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.Forall₂ R l₁.reverse l₂.reverse ↔ List.Forall₂ R l₁ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<GOAL>(List.Forall₂ (List.Forall₂ R) ⇒ List.Forall₂ R) List.join List.join
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R : α → β → Prop<VAR>P : γ → δ → Prop<GOAL>(List.Forall₂ R ⇒ (R ⇒ List.Forall₂ P) ⇒ List.Forall₂ P) List.bind List.bind
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R : α → β → Prop<VAR>P : γ → δ → Prop<GOAL>((P ⇒ R ⇒ P) ⇒ P ⇒ List.Forall₂ R ⇒ P) List.foldl List.foldl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R : α → β → Prop<VAR>P : γ → δ → Prop<GOAL>((R ⇒ P ⇒ P) ⇒ P ⇒ List.Forall₂ R ⇒ P) List.foldr List.foldr
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>p : α → Bool<VAR>q : β → Bool<VAR>hpq : (R ⇒ fun x x_1 => x ↔ x_1) (fun x => p x = true) fun x => q x = true<GOAL>(List.Forall₂ R ⇒ List.Forall₂ R) (List.filter p) (List.filter q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R : α → β → Prop<VAR>P : γ → δ → Prop<GOAL>((R ⇒ Option.Rel P) ⇒ List.Forall₂ R ⇒ List.Forall₂ P) List.filterMap List.filterMap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.SublistForall₂ R l₁ l₂ ↔ ∃ l, List.Forall₂ R l₁ l ∧ l.Sublist l₂
<VAR>α : Type u_1<VAR>Rₐ : α → α → Prop<VAR>l₁ l₂ : List α<VAR>h : l₁.Sublist l₂<VAR>IsRefl α Rₐ<GOAL>List.SublistForall₂ Rₐ l₁ l₂
<VAR>α : Type u_1<VAR>Rₐ : α → α → Prop<VAR>IsRefl α Rₐ<VAR>l : List α<GOAL>List.SublistForall₂ Rₐ l.tail l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r : List β<VAR>ys : List α<VAR>f : List α → β<GOAL>(List.permutationsAux2 t ts r ys f).1 = ys ++ ts
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r : List β<VAR>f : List α → β<GOAL>(List.permutationsAux2 t ts r [] f).2 = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r : List β<VAR>y : α<VAR>ys : List α<VAR>f : List α → β<GOAL>(List.permutationsAux2 t ts r (y :: ys) f).2 = f (t :: y :: ys ++ ts) :: (List.permutationsAux2 t ts r ys fun x => f (y :: x)).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r : List β<VAR>ys : List α<VAR>f : List α → β<GOAL>(List.permutationsAux2 t ts [] ys f).2 ++ r = (List.permutationsAux2 t ts r ys f).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts ys : List α<VAR>r : List β<VAR>f : List α → β<GOAL>(List.permutationsAux2 t [] r ys fun x => f (x ++ ts)).2 = (List.permutationsAux2 t ts r ys f).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>α' : Type u_3<VAR>β' : Type u_4<VAR>g : α → α'<VAR>g' : β → β'<VAR>t : α<VAR>ts ys : List α<VAR>r : List β<VAR>f : List α → β<VAR>f' : List α' → β'<VAR>H : ∀ (a : List α), g' (f a) = f' (List.map g a)<GOAL>List.map g' (List.permutationsAux2 t ts r ys f).2 = (List.permutationsAux2 (g t) (List.map g ts) (List.map g' r) (List.map g ys) f').2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts ys : List α<VAR>f : List α → β<GOAL>List.map f (List.permutationsAux2 t ts [] ys id).2 = (List.permutationsAux2 t ts [] ys f).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r : List β<VAR>ys : List α<VAR>f : List α → β<GOAL>(List.permutationsAux2 t ts r ys f).2 = List.map (fun x => f (x ++ ts)) (List.permutationsAux2 t [] [] ys id).2 ++ r
<VAR>α : Type u_1<VAR>α' : Type u_3<VAR>g : α → α'<VAR>t : α<VAR>ts ys : List α<GOAL>List.map (List.map g) (List.permutationsAux2 t ts [] ys id).2 = (List.permutationsAux2 (g t) (List.map g ts) [] (List.map g ys) id).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>t : α<VAR>ts : List α<GOAL>List.map (List.map f) (List.permutations'Aux t ts) = List.permutations'Aux (f t) (List.map f ts)
<VAR>α : Type u_1<VAR>t : α<VAR>ts : List α<GOAL>List.permutations'Aux t ts = (List.permutationsAux2 t [] [ts ++ [t]] ts id).2
<VAR>α : Type u_1<VAR>t : α<VAR>ts ys l l' : List α<GOAL>l' ∈ (List.permutationsAux2 t ts [] ys fun x => l ++ x).2 ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
<VAR>α : Type u_1<VAR>t : α<VAR>ts ys l : List α<GOAL>l ∈ (List.permutationsAux2 t ts [] ys id).2 ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts ys : List α<VAR>f : List α → β<GOAL>(List.permutationsAux2 t ts [] ys f).2.length = ys.length
<VAR>α : Type u_1<VAR>t : α<VAR>ts : List α<VAR>r L : List (List α)<GOAL>List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) r L = (L.bind fun y => (List.permutationsAux2 t ts [] y id).2) ++ r
<VAR>α : Type u_1<VAR>t : α<VAR>ts : List α<VAR>r L : List (List α)<VAR>l' : List α<GOAL>l' ∈ List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) r L ↔ l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
<VAR>α : Type u_1<VAR>t : α<VAR>ts : List α<VAR>r L : List (List α)<GOAL>(List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) r L).length = Nat.sum (List.map List.length L) + r.length
<VAR>α : Type u_1<VAR>t : α<VAR>ts : List α<VAR>r L : List (List α)<VAR>n : ℕ<VAR>H : ∀ (l : List α), l ∈ L → l.length = n<GOAL>(List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) r L).length = n * L.length + r.length
<VAR>α : Type u_1<VAR>is : List α<GOAL>[].permutationsAux is = []
<VAR>α : Type u_1<VAR>t : α<VAR>ts is : List α<GOAL>(t :: ts).permutationsAux is = List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) (ts.permutationsAux (t :: is)) is.permutations
<VAR>α : Type u_1<GOAL>[].permutations = [[]]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ts is : List α<GOAL>List.map (List.map f) (ts.permutationsAux is) = (List.map f ts).permutationsAux (List.map f is)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ts : List α<GOAL>List.map (List.map f) ts.permutations = (List.map f ts).permutations
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ts : List α<GOAL>List.map (List.map f) ts.permutations' = (List.map f ts).permutations'
<VAR>α : Type u_1<VAR>is is' ts : List α<GOAL>(is ++ ts).permutationsAux is' = List.map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
<VAR>α : Type u_1<VAR>is ts : List α<GOAL>(is ++ ts).permutations = List.map (fun x => x ++ ts) is.permutations ++ ts.permutationsAux is.reverse
<VAR>α : Type u<VAR>Preorder α<VAR>l : List α<VAR>h : List.Sorted (fun x x_1 => x < x_1) l<GOAL>List.Sorted (fun x x_1 => x ≤ x_1) l
<VAR>α : Type u<VAR>PartialOrder α<VAR>l : List α<VAR>h₁ : List.Sorted (fun x x_1 => x ≤ x_1) l<VAR>h₂ : l.Nodup<GOAL>List.Sorted (fun x x_1 => x < x_1) l
<VAR>α : Type u<VAR>Preorder α<VAR>l : List α<VAR>h : List.Sorted (fun x x_1 => x > x_1) l<GOAL>List.Sorted (fun x x_1 => x ≥ x_1) l
<VAR>α : Type u<VAR>PartialOrder α<VAR>l : List α<VAR>h₁ : List.Sorted (fun x x_1 => x ≥ x_1) l<VAR>h₂ : l.Nodup<GOAL>List.Sorted (fun x x_1 => x > x_1) l
<VAR>α : Type u<VAR>r : α → α → Prop<GOAL>List.Sorted r []
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a : α<VAR>l : List α<GOAL>List.Sorted r (a :: l) → List.Sorted r l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>l : List α<VAR>h : List.Sorted r l<GOAL>List.Sorted r l.tail
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a : α<VAR>l : List α<GOAL>List.Sorted r (a :: l) → ∀ b ∈ l, r a b
<VAR>α : Type u<VAR>Inhabited α<VAR>Preorder α<VAR>a : α<VAR>l : List α<VAR>h : List.Sorted (fun x x_1 => x < x_1) l<VAR>ha : a ∈ l<GOAL>l.head! ≤ a
<VAR>α : Type u<VAR>Inhabited α<VAR>Preorder α<VAR>a : α<VAR>l : List α<VAR>h : List.Sorted (fun x x_1 => x > x_1) l<VAR>ha : a ∈ l<GOAL>a ≤ l.head!
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a : α<VAR>l : List α<GOAL>List.Sorted r (a :: l) ↔ (∀ b ∈ l, r a b) ∧ List.Sorted r l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsIrrefl α r<VAR>l : List α<VAR>h : List.Sorted r l<GOAL>l.Nodup
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsAntisymm α r<VAR>l₁ l₂ : List α<VAR>hp : l₁.Perm l₂<VAR>hs₁ : List.Sorted r l₁<VAR>hs₂ : List.Sorted r l₂<GOAL>l₁ = l₂
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsAntisymm α r<VAR>l₁ l₂ : List α<VAR>hp : l₁.Subperm l₂<VAR>hs₁ : List.Sorted r l₁<VAR>hs₂ : List.Sorted r l₂<GOAL>l₁.Sublist l₂
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a : α<GOAL>List.Sorted r [a]
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>l : List α<VAR>h : List.Sorted r l<VAR>a b : Fin l.length<VAR>hab : a < b<GOAL>r (l.get a) (l.get b)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>l : List α<VAR>h : List.Sorted r l<VAR>a b : ℕ<VAR>ha : a < l.length<VAR>hb : b < l.length<VAR>hab : a < b<GOAL>r (l.nthLe a ha) (l.nthLe b hb)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>l : List α<VAR>h : List.Sorted r l<VAR>a b : Fin l.length<VAR>hab : a ≤ b<GOAL>r (l.get a) (l.get b)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>l : List α<VAR>h : List.Sorted r l<VAR>a b : ℕ<VAR>ha : a < l.length<VAR>hb : b < l.length<VAR>hab : a ≤ b<GOAL>r (l.nthLe a ha) (l.nthLe b hb)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>l : List α<VAR>h : List.Sorted r l<VAR>k : ℕ<VAR>x y : α<VAR>hx : x ∈ List.take k l<VAR>hy : y ∈ List.drop k l<GOAL>r x y
<VAR>n : ℕ<VAR>α : Type u<VAR>f : Fin n → α<VAR>r : α → α → Prop<GOAL>List.Sorted r (List.ofFn f) ↔ ((fun x x_1 => x < x_1) ⇒ r) f f
<VAR>n : ℕ<VAR>α : Type u<VAR>f : Fin n → α<VAR>Preorder α<GOAL>List.Sorted (fun x x_1 => x < x_1) (List.ofFn f) ↔ StrictMono f
<VAR>n : ℕ<VAR>α : Type u<VAR>f : Fin n → α<VAR>Preorder α<GOAL>List.Sorted (fun x x_1 => x ≤ x_1) (List.ofFn f) ↔ Monotone f
<VAR>n : ℕ<VAR>α : Type u<VAR>f : Fin n → α<VAR>Preorder α<GOAL>Monotone f ↔ List.Sorted (fun x x_1 => x ≤ x_1) (List.ofFn f)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>a : α<GOAL>List.orderedInsert r a [] = [a]
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>L : List α<VAR>a : α<GOAL>(List.orderedInsert r a L).length = L.length + 1
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>a : α<VAR>l : List α<GOAL>List.orderedInsert r a l = List.takeWhile (fun b => decide ¬r a b) l ++ a :: List.dropWhile (fun b => decide ¬r a b) l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>a : α<VAR>l : List α<GOAL>List.insertionSort r (a :: l) = List.takeWhile (fun b => decide ¬r a b) (List.insertionSort r l) ++ a :: List.dropWhile (fun b => decide ¬r a b) (List.insertionSort r l)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>a b : α<VAR>l : List α<GOAL>a ∈ List.orderedInsert r b l ↔ a = b ∨ a ∈ l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>a : α<VAR>l : List α<GOAL>(List.orderedInsert r a l).Perm (a :: l)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>DecidableEq α<VAR>L : List α<VAR>a b : α<GOAL>List.count a (List.orderedInsert r b L) = List.count a L + if a = b then 1 else 0
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>l : List α<GOAL>(List.insertionSort r l).Perm l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>l : List α<GOAL>List.Sorted r l → List.insertionSort r l = l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>DecidableEq α<VAR>IsRefl α r<VAR>x : α<VAR>xs : List α<GOAL>(List.orderedInsert r x xs).erase x = xs
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>DecidableEq α<VAR>x : α<VAR>xs : List α<VAR>hx : x ∉ xs<GOAL>(List.orderedInsert r x xs).erase x = xs
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>DecidableEq α<VAR>IsAntisymm α r<VAR>x : α<VAR>xs : List α<VAR>hx : x ∈ xs<VAR>hxs : List.Sorted r xs<GOAL>List.orderedInsert r x (xs.erase x) = xs
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>x : α<VAR>xs : List α<GOAL>xs.Sublist (List.orderedInsert r x xs)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTotal α r<VAR>IsTrans α r<VAR>a : α<VAR>l : List α<GOAL>List.Sorted r l → List.Sorted r (List.orderedInsert r a l)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTotal α r<VAR>IsTrans α r<VAR>l : List α<GOAL>List.Sorted r (List.insertionSort r l)
<VAR>α : Type u<VAR>a : α<VAR>l l₁ l₂ : List α<VAR>h : l.split = (l₁, l₂)<GOAL>(a :: l).split = (a :: l₂, l₁)
<VAR>α : Type u<VAR>l l₁ l₂ : List α<GOAL>l.split = (l₁, l₂) → l₁.length ≤ l.length ∧ l₂.length ≤ l.length
<VAR>α : Type u<VAR>l : List α<GOAL>l.split.1.length ≤ l.length
<VAR>α : Type u<VAR>l : List α<GOAL>l.split.2.length ≤ l.length
<VAR>α : Type u<VAR>a b : α<VAR>l l₁ l₂ : List α<VAR>h : (a :: b :: l).split = (l₁, l₂)<GOAL>l₁.length < (a :: b :: l).length ∧ l₂.length < (a :: b :: l).length
<VAR>α : Type u<VAR>l l₁ l₂ : List α<GOAL>l.split = (l₁, l₂) → l.Perm (l₁ ++ l₂)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>a b : α<VAR>l l₁ l₂ : List α<VAR>h : (a :: b :: l).split = (l₁, l₂)<GOAL>List.mergeSort r (a :: b :: l) = List.merge (fun x x_1 => decide (r x x_1)) (List.mergeSort r l₁) (List.mergeSort r l₂)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>l : List α<GOAL>(List.mergeSort r l).Perm l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>l : List α<GOAL>(List.mergeSort r l).length = l.length
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTotal α r<VAR>IsTrans α r<VAR>l l' : List α<GOAL>List.Sorted r l → List.Sorted r l' → List.Sorted r (List.merge (fun x x_1 => decide (r x x_1)) l l')
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTotal α r<VAR>IsTrans α r<VAR>l : List α<GOAL>List.Sorted r (List.mergeSort r l)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTotal α r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>l : List α<GOAL>List.Sorted r l → List.mergeSort r l = l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTotal α r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>l : List α<GOAL>List.mergeSort r l = List.insertionSort r l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<GOAL>List.mergeSort r [] = []
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>a : α<GOAL>List.mergeSort r [a] = [a]
<VAR>α : Type u<VAR>l : List α<GOAL>(Batteries.DList.ofList l).toList = l
<VAR>α : Type u<VAR>l : Batteries.DList α<GOAL>Batteries.DList.ofList l.toList = l
<VAR>α : Type u<GOAL>Batteries.DList.empty.toList = []
<VAR>α : Type u<VAR>x : α<GOAL>(Batteries.DList.singleton x).toList = [x]
<VAR>α : Type u<VAR>l₁ l₂ : Batteries.DList α<GOAL>(l₁ ++ l₂).toList = l₁.toList ++ l₂.toList
<VAR>α : Type u<VAR>x : α<VAR>l : Batteries.DList α<GOAL>(Batteries.DList.cons x l).toList = x :: l.toList
<VAR>α : Type u<VAR>x : α<VAR>l : Batteries.DList α<GOAL>(l.push x).toList = l.toList ++ [x]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : ℕ → α → β<GOAL>List.mapIdx f [] = []
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : ℕ → α → β<VAR>n : ℕ<GOAL>List.oldMapIdxCore f n l = List.oldMapIdx (fun i a => f (i + n) a) l
<VAR>α : Type u<VAR>p : List α → Prop<VAR>base : p []<VAR>ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])<VAR>l : List α<GOAL>p l
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>n : ℕ<VAR>l₁ l₂ : List α<GOAL>List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>l : List α<VAR>e : α<GOAL>List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f l.length e]
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>l₁ l₂ : List α<VAR>arr : Array β<GOAL>List.mapIdx.go f (l₁ ++ l₂) arr = List.mapIdx.go f l₂ (List.toArray (List.mapIdx.go f l₁ arr))
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>l : List α<VAR>arr : Array β<GOAL>(List.mapIdx.go f l arr).length = l.length + arr.size
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>l : List α<VAR>e : α<GOAL>List.mapIdx f (l ++ [e]) = List.mapIdx f l ++ [f l.length e]
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>l : List α<GOAL>List.mapIdx f l = List.oldMapIdx f l
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>n : ℕ<VAR>f : ℕ → α → β<GOAL>List.map (Function.uncurry f) (List.enumFrom n l) = List.zipWith (fun i => f (i + n)) (List.range l.length) l
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : ℕ → α → β<GOAL>List.mapIdx f l = List.map (Function.uncurry f) l.enum
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : ℕ → α → β<VAR>a : α<GOAL>List.mapIdx f (a :: l) = f 0 a :: List.mapIdx (fun i => f (i + 1)) l