ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_2<VAR>AddZeroClass R<VAR>l₁ l₂ : List R<VAR>DecidablePred fun x => (l₁ ++ l₂).getD x 0 ≠ 0<VAR>DecidablePred fun x => l₁.getD x 0 ≠ 0<VAR>DecidablePred fun x => l₂.getD x 0 ≠ 0<GOAL>(l₁ ++ l₂).toFinsupp = l₁.toFinsupp + Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp
<VAR>R : Type u_2<VAR>AddZeroClass R<VAR>x : R<VAR>xs : List R<VAR>DecidablePred fun x_1 => (x :: xs).getD x_1 0 ≠ 0<VAR>DecidablePred fun x => xs.getD x 0 ≠ 0<GOAL>(x :: xs).toFinsupp = Finsupp.single 0 x + Finsupp.embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } xs.toFinsupp
<VAR>R : Type u_2<VAR>AddZeroClass R<VAR>x : R<VAR>xs : List R<VAR>DecidablePred fun i => (xs ++ [x]).getD i 0 ≠ 0<VAR>DecidablePred fun i => xs.getD i 0 ≠ 0<GOAL>(xs ++ [x]).toFinsupp = xs.toFinsupp + Finsupp.single xs.length x
<VAR>R : Type u_2<VAR>AddMonoid R<VAR>l : List R<VAR>DecidablePred fun x => l.getD x 0 ≠ 0<GOAL>l.toFinsupp = (List.map (fun nr => Finsupp.single nr.1 nr.2) l.enum).sum
<VAR>M : Type u_1<VAR>CommMonoidWithZero M<VAR>p : M<VAR>L : List M<VAR>pp : Prime p<GOAL>p ∣ L.prod ↔ ∃ a ∈ L, p ∣ a
<VAR>M : Type u_1<VAR>CommMonoidWithZero M<VAR>p : M<VAR>L : List M<VAR>pp : Prime p<VAR>hL : ∀ a ∈ L, ¬p ∣ a<GOAL>¬p ∣ L.prod
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>Unique Mˣ<VAR>p : M<VAR>hp : Prime p<VAR>L : List M<VAR>hL : ∀ q ∈ L, Prime q<VAR>hpL : p ∣ L.prod<GOAL>p ∈ L
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>Unique Mˣ<VAR>l₁ l₂ : List M<GOAL>l₁.prod = l₂.prod → (∀ p ∈ l₁, Prime p) → (∀ p ∈ l₂, Prime p) → l₁ ~ l₂
<VAR>α : Type u_1<VAR>l : List α<GOAL>[l].join = l
<VAR>α : Type u_1<VAR>L : List (List α)<GOAL>L.join = [] ↔ ∀ (l : List α), l ∈ L → l = []
<VAR>α : Type u_1<VAR>L₁ L₂ : List (List α)<GOAL>(L₁ ++ L₂).join = L₁.join ++ L₂.join
<VAR>α : Type u_1<VAR>L : List (List α)<VAR>l : List α<GOAL>(L.concat l).join = L.join ++ l
<VAR>α : Type u_1<VAR>L : List (List α)<GOAL>(List.filter (fun l => !l.isEmpty) L).join = L.join
<VAR>α : Type u_1<VAR>DecidablePred fun l => l ≠ []<VAR>L : List (List α)<GOAL>(List.filter (fun l => decide (l ≠ [])) L).join = L.join
<VAR>α : Type u_1<VAR>l : List (List (List α))<GOAL>l.join.join = (List.map List.join l).join
<VAR>α : Type u_1<VAR>L : List (List α)<GOAL>L.join.length = Nat.sum (List.map List.length L)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>L : List (List α)<GOAL>List.countP p L.join = Nat.sum (List.map (List.countP p) L)
<VAR>α : Type u_1<VAR>BEq α<VAR>L : List (List α)<VAR>a : α<GOAL>List.count a L.join = Nat.sum (List.map (List.count a) L)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f : α → List β<GOAL>(l.bind f).length = Nat.sum (List.map (List.length ∘ f) l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : β → Bool<VAR>l : List α<VAR>f : α → List β<GOAL>List.countP p (l.bind f) = Nat.sum (List.map (List.countP p ∘ f) l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq β<VAR>l : List α<VAR>f : α → List β<VAR>x : β<GOAL>List.count x (l.bind f) = Nat.sum (List.map (List.count x ∘ f) l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f : α → List β<GOAL>l.bind f = [] ↔ ∀ (x : α), x ∈ l → f x = []
<VAR>α : Type u_1<VAR>L : List (List α)<VAR>i : ℕ<GOAL>List.take (Nat.sum (List.take i (List.map List.length L))) L.join = (List.take i L).join
<VAR>α : Type u_1<VAR>L : List (List α)<VAR>i : ℕ<GOAL>List.drop (Nat.sum (List.take i (List.map List.length L))) L.join = (List.drop i L).join
<VAR>α : Type u_1<VAR>L : List α<VAR>i : ℕ<VAR>h : i < L.length<GOAL>List.drop i (List.take (i + 1) L) = [L[i]]
<VAR>α : Type u_1<VAR>L : List α<VAR>i : Fin L.length<GOAL>List.drop (↑i) (List.take (↑i + 1) L) = [L.get i]
<VAR>α : Type u_1<VAR>L : List α<VAR>i : ℕ<VAR>hi : i < L.length<GOAL>List.drop i (List.take (i + 1) L) = [L.nthLe i hi]
<VAR>α : Type u_1<VAR>L : List (List α)<VAR>i : ℕ<VAR>h : i < L.length<GOAL>List.drop (Nat.sum (List.take i (List.map List.length L))) (List.take (Nat.sum (List.take (i + 1) (List.map List.length L))) L.join) = L[i]
<VAR>α : Type u_1<VAR>L : List (List α)<VAR>i : Fin L.length<GOAL>List.drop (Nat.sum (List.take (↑i) (List.map List.length L))) (List.take (Nat.sum (List.take (↑i + 1) (List.map List.length L))) L.join) = L.get i
<VAR>α : Type u_1<VAR>L L' : List (List α)<GOAL>L = L' ↔ L.join = L'.join ∧ List.map List.length L = List.map List.length L'
<VAR>α : Type u_1<VAR>L : List (List α)<VAR>h : L ≠ []<GOAL>(List.drop (L.length - 1) L).join = L.getLast h
<VAR>α : Type u_1<VAR>L : List (List α)<VAR>x : List α<GOAL>x ++ (List.map (fun x_1 => x_1 ++ x) L).join = (List.map (fun x_1 => x ++ x_1) L).join ++ x
<VAR>α : Type u_1<VAR>L : List (List α)<GOAL>L.join.reverse = (List.map List.reverse L).reverse.join
<VAR>α : Type u_1<VAR>L : List (List α)<GOAL>L.reverse.join = (List.map List.reverse L).join.reverse
<VAR>α : Type u_1<VAR>L : List (List α)<VAR>s : List α<VAR>hs : s ∈ L<GOAL>s.Sublist L.join
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>[].dedup = []
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l.dedup<GOAL>(a :: l).dedup = l.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∉ l.dedup<GOAL>(a :: l).dedup = a :: l.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>a ∈ l.dedup ↔ a ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>(a :: l).dedup = l.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∉ l<GOAL>(a :: l).dedup = a :: l.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.dedup.Sublist l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.dedup ⊆ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l ⊆ l.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.dedup.Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Inhabited α<VAR>l : List α<GOAL>l.dedup.headI = if l.headI ∈ l.tail then l.tail.dedup.headI else l.headI
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Inhabited α<VAR>l : List α<GOAL>l.dedup.tail = if l.headI ∈ l.tail then l.tail.dedup.tail else l.tail.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.dedup = l ↔ l.Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<VAR>l' : List α<GOAL>l.dedup = a :: l' ↔ a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.dedup = [] ↔ l = []
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<GOAL>l.dedup = l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.dedup.dedup = l.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>xs : List α<GOAL>(List.map f xs).dedup = List.map f xs.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs ys : List α<VAR>h : xs ⊆ ys<GOAL>(xs ++ ys).dedup = ys.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs ys : List α<VAR>h : xs.Disjoint ys<GOAL>xs ∪ ys = xs.dedup ++ ys
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs ys : List α<VAR>h : xs.Disjoint ys<GOAL>(xs ++ ys).dedup = xs.dedup ++ ys.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x : α<VAR>k : ℕ<GOAL>k ≠ 0 → (List.replicate k x).dedup = [x]
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>List.count a l.dedup = if a ∈ l then 1 else 0
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsIrrefl α r<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>List.Lex r (a :: l₁) (a :: l₂) ↔ List.Lex r l₁ l₂
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>l : List α<GOAL>¬List.Lex r l []
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>l : List α<GOAL>List.Lex r [] l ∨ l = []
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<GOAL>List.Lex r [a] [b] ↔ r a b
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsOrderConnected α r<VAR>IsTrichotomous α r<GOAL>∀ (x x_1 x_2 : List α), List.Lex r x x_2 → List.Lex r x x_1 ∨ List.Lex r x_1 x_2
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsTrichotomous α r<GOAL>∀ (x x_1 : List α), List.Lex r x x_1 ∨ x = x_1 ∨ List.Lex r x_1 x
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsAsymm α r<GOAL>∀ (x x_1 : List α), List.Lex r x x_1 → List.Lex r x_1 x → False
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>s₁ s₂ : List α<VAR>t : List α<GOAL>List.Lex r s₁ s₂ → List.Lex r s₁ (s₂ ++ t)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>t₁ t₂ : List α<VAR>h : List.Lex R t₁ t₂<VAR>s : List α<GOAL>List.Lex R (s ++ t₁) (s ++ t₂)
<VAR>α : Type u<VAR>r s : α → α → Prop<VAR>H : ∀ (a b : α), r a b → s a b<VAR>l₁ l₂ : List α<GOAL>List.Lex r l₁ l₂ → List.Lex s l₁ l₂
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>List.Lex (fun x x_1 => x ≠ x_1) l₁ l₂ → l₁ ≠ l₂
<VAR>α : Type u<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>H : l₁.length ≤ l₂.length<GOAL>List.Lex (fun x x_1 => x ≠ x_1) l₁ l₂ ↔ l₁ ≠ l₂
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>H : l₁.length ≤ l₂.length<GOAL>List.Lex (fun x x_1 => x ≠ x_1) l₁ l₂ ↔ l₁ ≠ l₂
<VAR>α : Type u<VAR>LT α<VAR>a : α<VAR>l : List α<GOAL>[] < a :: l
<VAR>α : Type u<VAR>LinearOrder α<VAR>l l' : List α<GOAL>l.lt l' ↔ List.Lex (fun x x_1 => x < x_1) l l'
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<GOAL>[] ≤ l
<VAR>α : Type u<VAR>Preorder α<VAR>a a' : α<VAR>l l' : List α<VAR>h : a' :: l' < a :: l<GOAL>a' ≤ a
<VAR>α : Type u<VAR>Preorder α<VAR>Inhabited α<VAR>l l' : List α<VAR>h : l' < l<VAR>hl' : l' ≠ []<GOAL>l'.head! ≤ l.head!
<VAR>α : Type u<VAR>LinearOrder α<VAR>a : α<VAR>l l' : List α<VAR>h : l' ≤ l<GOAL>a :: l' ≤ a :: l
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i j : ℕ<VAR>h : i + j = n<GOAL>(List.ofFn.go f i j h).length = i
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>(List.ofFn f).length = n
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i j : ℕ<VAR>h : i + j = n<VAR>k : ℕ<VAR>hk : k < (List.ofFn.go f i j h).length<GOAL>(List.ofFn.go f i j h)[k] = f ⟨j + k, ⋯⟩
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i j : ℕ<VAR>h : i + j = n<VAR>k : ℕ<VAR>hk : k < (List.ofFn.go f i j h).length<GOAL>(List.ofFn.go f i j h).get ⟨k, hk⟩ = f ⟨j + k, ⋯⟩
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : ℕ<VAR>h : i < (List.ofFn f).length<GOAL>(List.ofFn f)[i] = f ⟨i, ⋯⟩
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : Fin (List.ofFn f).length<GOAL>(List.ofFn f).get i = f (Fin.cast ⋯ i)
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : ℕ<GOAL>(List.ofFn f)[i]? = List.ofFnNthVal f i
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : ℕ<GOAL>(List.ofFn f).get? i = List.ofFnNthVal f i
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : Fin n<GOAL>(List.ofFn f).nthLe ↑i ⋯ = f i
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : ℕ<VAR>h : i < (List.ofFn f).length<GOAL>(List.ofFn f).nthLe i h = f ⟨i, ⋯⟩
<VAR>α : Type u<VAR>β : Type u_1<VAR>n : ℕ<VAR>f : Fin n → α<VAR>g : α → β<GOAL>List.map g (List.ofFn f) = List.ofFn (g ∘ f)
<VAR>α : Type u<VAR>m n : ℕ<VAR>h : m = n<VAR>f : Fin m → α<GOAL>List.ofFn f = List.ofFn fun i => f (Fin.cast ⋯ i)
<VAR>α : Type u<VAR>f : Fin 0 → α<GOAL>List.ofFn f = []
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n.succ → α<GOAL>List.ofFn f = f 0 :: List.ofFn fun i => f i.succ
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n.succ → α<GOAL>List.ofFn f = (List.ofFn fun i => f i.castSucc).concat (f (Fin.last n))
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>List.ofFn f = [] ↔ n = 0
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>h : List.ofFn f ≠ []<VAR>hn : n - 1 < n := ⋯<GOAL>(List.ofFn f).getLast h = f ⟨n - 1, hn⟩
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n.succ → α<VAR>h : List.ofFn f ≠ [] := ⋯<GOAL>(List.ofFn f).getLast h = f (Fin.last n)
<VAR>α : Type u<VAR>m n : ℕ<VAR>f : Fin (m + n) → α<GOAL>List.ofFn f = (List.ofFn fun i => f (Fin.castAdd n i)) ++ List.ofFn fun j => f (Fin.natAdd m j)
<VAR>α : Type u<VAR>m n : ℕ<VAR>a : Fin m → α<VAR>b : Fin n → α<GOAL>List.ofFn (Fin.append a b) = List.ofFn a ++ List.ofFn b
<VAR>α : Type u<VAR>m n : ℕ<VAR>f : Fin (m * n) → α<GOAL>List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).join
<VAR>α : Type u<VAR>m n : ℕ<VAR>f : Fin (m * n) → α<GOAL>List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨m * ↑i + ↑j, ⋯⟩).join
<VAR>α : Type u<VAR>l : List α<GOAL>List.ofFn l.get = l
<VAR>α : Type u<VAR>l : List α<GOAL>(List.ofFn fun i => l[↑i]) = l
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List α<VAR>f : α → β<GOAL>(List.ofFn fun i => f l[↑i]) = List.map f l
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List α<VAR>f : α → β<GOAL>(List.ofFn fun x => f (l.get x)) = List.map f l
<VAR>α : Type u<VAR>l : List α<GOAL>(List.ofFn fun i => l.nthLe ↑i ⋯) = l
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>a : α<GOAL>a ∈ List.ofFn f ↔ a ∈ Set.range f
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>P : α → Prop<GOAL>(∀ i ∈ List.ofFn f, P i) ↔ ∀ (j : Fin n), P (f j)
<VAR>α : Type u<VAR>n : ℕ<VAR>c : α<GOAL>(List.ofFn fun x => c) = List.replicate n c
<VAR>α : Type u<VAR>m : ℕ<VAR>a : Fin m → α<VAR>n : ℕ<GOAL>List.ofFn (Fin.repeat n a) = (List.replicate n (List.ofFn a)).join
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>List.Pairwise R (List.ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)
<VAR>α : Type u<VAR>f : (n : ℕ) × (Fin n → α)<GOAL>List.equivSigmaTuple.symm f = List.ofFn f.snd
<VAR>α : Type u<VAR>l : List α<GOAL>∀ (a : Fin l.length), (List.equivSigmaTuple l).snd a = l.get a
<VAR>α : Type u<VAR>l : List α<GOAL>(List.equivSigmaTuple l).fst = l.length
<VAR>α : Type u<VAR>C : List α → Sort u_1<VAR>h : (n : ℕ) → (f : Fin n → α) → C (List.ofFn f)<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>List.ofFnRec h (List.ofFn f) = h n f
<VAR>α : Type u<VAR>P : List α → Prop<GOAL>(∃ l, P l) ↔ ∃ n f, P (List.ofFn f)
<VAR>α : Type u<VAR>P : List α → Prop<GOAL>(∀ (l : List α), P l) ↔ ∀ (n : ℕ) (f : Fin n → α), P (List.ofFn f)
<VAR>α : Type u<VAR>m n : ℕ<VAR>f : Fin m → α<VAR>g : Fin n → α<GOAL>List.ofFn f = List.ofFn g ↔ ⟨m, f⟩ = ⟨n, g⟩
<VAR>α : Type u<VAR>n : ℕ<GOAL>Function.Injective List.ofFn
<VAR>α : Type u<VAR>n : ℕ<VAR>f g : Fin n → α<GOAL>List.ofFn f = List.ofFn g ↔ f = g
<VAR>α : Type u<VAR>s : List α<VAR>x : α<GOAL>List.insertNth 0 x s = x :: s
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<GOAL>List.insertNth (n + 1) a [] = []
<VAR>α : Type u<VAR>s : List α<VAR>hd x : α<VAR>n : ℕ<GOAL>List.insertNth (n + 1) x (hd :: s) = hd :: List.insertNth n x s
<VAR>α : Type u<VAR>a : α<VAR>n : ℕ<VAR>as : List α<GOAL>n ≤ as.length → (List.insertNth n a as).length = as.length + 1
<VAR>α : Type u<VAR>a : α<VAR>n : ℕ<VAR>l : List α<GOAL>(List.insertNth n a l).eraseIdx n = l
<VAR>α : Type u<VAR>a : α<VAR>n m : ℕ<VAR>as : List α<GOAL>n < as.length → n ≤ m → List.insertNth m a (as.eraseIdx n) = (List.insertNth (m + 1) a as).eraseIdx n
<VAR>α : Type u<VAR>a : α<VAR>n m : ℕ<VAR>as : List α<GOAL>n < as.length → m ≤ n → List.insertNth m a (as.eraseIdx n) = (List.insertNth m a as).eraseIdx (n + 1)
<VAR>α : Type u<VAR>a b : α<VAR>i j : ℕ<VAR>l : List α<GOAL>i ≤ j → j ≤ l.length → List.insertNth (j + 1) b (List.insertNth i a l) = List.insertNth i a (List.insertNth j b l)
<VAR>α : Type u<VAR>a b : α<VAR>n : ℕ<VAR>l : List α<GOAL>n ≤ l.length → (a ∈ List.insertNth n b l ↔ a = b ∨ a ∈ l)
<VAR>α : Type u<VAR>l : List α<VAR>x : α<VAR>n : ℕ<VAR>h : l.length < n<GOAL>List.insertNth n x l = l
<VAR>α : Type u<VAR>l : List α<VAR>x : α<GOAL>List.insertNth l.length x l = l ++ [x]
<VAR>α : Type u<VAR>l : List α<VAR>x : α<VAR>n : ℕ<GOAL>l.length ≤ (List.insertNth n x l).length
<VAR>α : Type u<VAR>l : List α<VAR>x : α<VAR>n : ℕ<GOAL>(List.insertNth n x l).length ≤ l.length + 1
<VAR>α : Type u<VAR>l : List α<VAR>x : α<VAR>n k : ℕ<VAR>hn : k < n<VAR>hk : k < l.length<VAR>hk' : k < (List.insertNth n x l).length := ⋯<GOAL>(List.insertNth n x l)[k] = l[k]
<VAR>α : Type u<VAR>l : List α<VAR>x : α<VAR>n k : ℕ<VAR>hn : k < n<VAR>hk : k < l.length<VAR>hk' : k < (List.insertNth n x l).length := ⋯<GOAL>(List.insertNth n x l).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩
<VAR>α : Type u<VAR>l : List α<VAR>x : α<VAR>n k : ℕ<GOAL>k < n → ∀ (hk : k < l.length) (hk' : optParam (k < (List.insertNth n x l).length) ⋯), (List.insertNth n x l).nthLe k hk' = l.nthLe k hk
<VAR>α : Type u<VAR>l : List α<VAR>x : α<VAR>n : ℕ<VAR>hn : n ≤ l.length<VAR>hn' : n < (List.insertNth n x l).length := ⋯<GOAL>(List.insertNth n x l)[n] = x
<VAR>α : Type u<VAR>l : List α<VAR>x : α<VAR>n : ℕ<VAR>hn : n ≤ l.length<VAR>hn' : n < (List.insertNth n x l).length := ⋯<GOAL>(List.insertNth n x l).get ⟨n, hn'⟩ = x
<VAR>α : Type u<VAR>l : List α<VAR>x : α<VAR>n : ℕ<VAR>hn : n ≤ l.length<VAR>hn' : n < (List.insertNth n x l).length := ⋯<GOAL>(List.insertNth n x l).nthLe n hn' = x
<VAR>α : Type u<VAR>l : List α<VAR>x : α<VAR>n k : ℕ<VAR>hk' : n + k < l.length<VAR>hk : n + k + 1 < (List.insertNth n x l).length := ⋯<GOAL>(List.insertNth n x l)[n + k + 1] = l[n + k]
<VAR>α : Type u<VAR>l : List α<VAR>x : α<VAR>n k : ℕ<VAR>hk' : n + k < l.length<VAR>hk : n + k + 1 < (List.insertNth n x l).length := ⋯<GOAL>(List.insertNth n x l).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩
<VAR>α : Type u<VAR>l : List α<VAR>x : α<VAR>n k : ℕ<VAR>hk' : n + k < l.length<VAR>hk : n + k + 1 < (List.insertNth n x l).length := ⋯<GOAL>(List.insertNth n x l).nthLe (n + k + 1) hk = l.nthLe (n + k) hk'
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<GOAL>Function.Injective (List.insertNth n x)
<VAR>n : ℕ<GOAL>List.Ico 0 n = List.range n
<VAR>n m : ℕ<GOAL>(List.Ico n m).length = m - n
<VAR>n m : ℕ<GOAL>List.Pairwise (fun x x_1 => x < x_1) (List.Ico n m)
<VAR>n m : ℕ<GOAL>(List.Ico n m).Nodup
<VAR>n m l : ℕ<GOAL>l ∈ List.Ico n m ↔ n ≤ l ∧ l < m
<VAR>n m : ℕ<VAR>h : m ≤ n<GOAL>List.Ico n m = []
<VAR>n m k : ℕ<GOAL>List.map (fun x => k + x) (List.Ico n m) = List.Ico (n + k) (m + k)
<VAR>n m k : ℕ<VAR>h₁ : k ≤ n<GOAL>List.map (fun x => x - k) (List.Ico n m) = List.Ico (n - k) (m - k)
<VAR>n : ℕ<GOAL>List.Ico n n = []
<VAR>n m : ℕ<GOAL>List.Ico n m = [] ↔ m ≤ n
<VAR>n m l : ℕ<VAR>hnm : n ≤ m<VAR>hml : m ≤ l<GOAL>List.Ico n m ++ List.Ico m l = List.Ico n l
<VAR>n m l : ℕ<GOAL>List.Ico n m ∩ List.Ico m l = []
<VAR>n m l : ℕ<GOAL>(List.Ico n m).bagInter (List.Ico m l) = []
<VAR>n : ℕ<GOAL>List.Ico n (n + 1) = [n]
<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>List.Ico n (m + 1) = List.Ico n m ++ [m]
<VAR>n m : ℕ<VAR>h : n < m<GOAL>List.Ico n m = n :: List.Ico (n + 1) m
<VAR>m : ℕ<VAR>h : 0 < m<GOAL>List.Ico (m - 1) m = [m - 1]
<VAR>n m : ℕ<GOAL>List.Chain' (fun a b => b = a.succ) (List.Ico n m)
<VAR>n m : ℕ<GOAL>m ∉ List.Ico n m
<VAR>n m l : ℕ<VAR>hml : m ≤ l<GOAL>List.filter (fun x => decide (x < l)) (List.Ico n m) = List.Ico n m
<VAR>n m l : ℕ<VAR>hln : l ≤ n<GOAL>List.filter (fun x => decide (x < l)) (List.Ico n m) = []
<VAR>n m l : ℕ<VAR>hlm : l ≤ m<GOAL>List.filter (fun x => decide (x < l)) (List.Ico n m) = List.Ico n l
<VAR>n m l : ℕ<GOAL>List.filter (fun x => decide (x < l)) (List.Ico n m) = List.Ico n (min m l)
<VAR>n m l : ℕ<VAR>hln : l ≤ n<GOAL>List.filter (fun x => decide (l ≤ x)) (List.Ico n m) = List.Ico n m
<VAR>n m l : ℕ<VAR>hml : m ≤ l<GOAL>List.filter (fun x => decide (l ≤ x)) (List.Ico n m) = []
<VAR>n m l : ℕ<VAR>hnl : n ≤ l<GOAL>List.filter (fun x => decide (l ≤ x)) (List.Ico n m) = List.Ico l m
<VAR>n m l : ℕ<GOAL>List.filter (fun x => decide (l ≤ x)) (List.Ico n m) = List.Ico (max n l) m
<VAR>n m : ℕ<VAR>hnm : n < m<GOAL>List.filter (fun x => decide (x < n + 1)) (List.Ico n m) = [n]
<VAR>n m : ℕ<VAR>hnm : n < m<GOAL>List.filter (fun x => decide (x ≤ n)) (List.Ico n m) = [n]
<VAR>n a b : ℕ<GOAL>n < a ∨ b ≤ n ∨ n ∈ List.Ico a b
<VAR>α : Type u_1<VAR>a : α<GOAL>Batteries.DList.singleton a = Batteries.DList.lazy_ofList { fn := fun x => [a] }
<VAR>α : Type u_1<VAR>l : List α<GOAL>Batteries.DList.lazy_ofList { fn := fun x => l } = Batteries.DList.ofList l
<VAR>α : Type u<VAR>β : Type u_1<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.map Prod.swap (l₁.zip l₂) = l₂.zip l₁
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>p : γ → Prop<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>l₁.length = l₂.length → (List.Forall p (List.zipWith f l₁ l₂) ↔ List.Forall₂ (fun x y => p (f x y)) l₁ l₂)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>i : ℕ<VAR>l : List α<VAR>l' : List β<VAR>h : i < (List.zipWith f l l').length<GOAL>i < l.length
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>i : ℕ<VAR>l : List α<VAR>l' : List β<VAR>h : i < (List.zipWith f l l').length<GOAL>i < l'.length
<VAR>α : Type u<VAR>β : Type u_1<VAR>i : ℕ<VAR>l : List α<VAR>l' : List β<VAR>h : i < (l.zip l').length<GOAL>i < l.length
<VAR>α : Type u<VAR>β : Type u_1<VAR>i : ℕ<VAR>l : List α<VAR>l' : List β<VAR>h : i < (l.zip l').length<GOAL>i < l'.length
<VAR>α : Type u<VAR>β : Type u_1<VAR>a : α<VAR>b : β<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>(a, b) ∈ l₁.zip l₂ → a ∈ l₁ ∧ b ∈ l₂
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List (α × β)<GOAL>l.unzip = (List.map Prod.fst l, List.map Prod.snd l)
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List (α × β)<GOAL>l.unzip.1 = List.map Prod.fst l
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List (α × β)<GOAL>l.unzip.2 = List.map Prod.snd l
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List (α × β)<GOAL>(List.map Prod.swap l).unzip = l.unzip.swap
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List (α × β)<GOAL>l.unzip.1.zip l.unzip.2 = l
<VAR>α : Type u<VAR>β : Type u_1<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>l₁.length ≤ l₂.length → (l₁.zip l₂).unzip.1 = l₁
<VAR>α : Type u<VAR>β : Type u_1<VAR>l₁ : List α<VAR>l₂ : List β<VAR>h : l₂.length ≤ l₁.length<GOAL>(l₁.zip l₂).unzip.2 = l₂
<VAR>α : Type u<VAR>β : Type u_1<VAR>l₁ : List α<VAR>l₂ : List β<VAR>h : l₁.length = l₂.length<GOAL>(l₁.zip l₂).unzip = (l₁, l₂)
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List α<VAR>l' : List β<VAR>lp : List (α × β)<VAR>hl : List.map Prod.fst lp = l<VAR>hr : List.map Prod.snd lp = l'<GOAL>lp = l.zip l'
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List α<VAR>f : α → β<GOAL>List.map (fun x => (x, f x)) l = l.zip (List.map f l)
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List α<VAR>f : α → β<GOAL>List.map (fun x => (f x, x)) l = (List.map f l).zip l
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>la : List α<VAR>lb : List β<GOAL>List.zipWith f la lb = List.zipWith (fun b a => f a b) lb la
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f g : α → β → γ<VAR>la : List α<VAR>lb : List β<VAR>h : List.Forall₂ (fun a b => f a b = g a b) la lb<GOAL>List.zipWith f la lb = List.zipWith g la lb
<VAR>α : Type u<VAR>β : Type u_1<VAR>f : α → α → β<VAR>comm : ∀ (x y : α), f x y = f y x<VAR>l l' : List α<GOAL>List.zipWith f l l' = List.zipWith f l' l
<VAR>α : Type u<VAR>δ : Type u_3<VAR>f : α → α → δ<VAR>l : List α<GOAL>List.zipWith f l l = List.map (fun a => f a a) l
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>la : List α<VAR>lb : List β<VAR>lc : List γ<GOAL>List.zipWith f (List.zipWith g la lb) lc = List.zipWith3 (fun a b c => f (g a b) c) la lb lc
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → δ → ε<VAR>g : β → γ → δ<VAR>la : List α<VAR>lb : List β<VAR>lc : List γ<GOAL>List.zipWith f la (List.zipWith g lb lc) = List.zipWith3 (fun a b c => f a (g b c)) la lb lc
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → α → β → γ<VAR>la : List α<VAR>lb : List β<GOAL>List.zipWith3 f la la lb = List.zipWith (fun a b => f a a b) la lb
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → α → γ<VAR>la : List α<VAR>lb : List β<GOAL>List.zipWith3 f la lb la = List.zipWith (fun a b => f a b a) la lb
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → β → γ<VAR>la : List α<VAR>lb : List β<GOAL>List.zipWith3 f la lb lb = List.zipWith (fun a b => f a b b) la lb
<VAR>α : Type u<VAR>l : List α<GOAL>l.revzip.length = l.length
<VAR>α : Type u<VAR>l : List α<GOAL>l.revzip.unzip = (l, l.reverse)
<VAR>α : Type u<VAR>l : List α<GOAL>List.map Prod.fst l.revzip = l
<VAR>α : Type u<VAR>l : List α<GOAL>List.map Prod.snd l.revzip = l.reverse
<VAR>α : Type u<VAR>l : List α<GOAL>l.revzip.reverse = l.reverse.revzip
<VAR>α : Type u<VAR>l : List α<GOAL>List.map Prod.swap l.revzip = l.reverse.revzip
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>l₁ : List α<VAR>l₂ : List β<VAR>i : ℕ<GOAL>(List.zipWith f l₁ l₂)[i]? = (Option.map f l₁[i]?).bind fun g => Option.map g l₂[i]?
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>l₁ : List α<VAR>l₂ : List β<VAR>i : ℕ<GOAL>(List.zipWith f l₁ l₂).get? i = (Option.map f (l₁.get? i)).bind fun g => Option.map g (l₂.get? i)