ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>h : s.Subsingleton<GOAL>StrictAntiOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>MonotoneOn f {a}
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>AntitoneOn f {a}
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictMonoOn f {a}
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictAntiOn f {a}
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>self : FiniteInter S<GOAL>Set.univ ∈ S
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>self : FiniteInter S<VAR>s : Set α<GOAL>s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
<VAR>α : Type u_1<VAR>S : Set (Set α)<GOAL>FiniteInter (FiniteInter.finiteInterClosure S)
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>cond : FiniteInter S<VAR>F : Finset (Set α)<GOAL>↑F ⊆ S → ⋂₀ ↑F ∈ S
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>A : Set α<VAR>cond : FiniteInter S<VAR>P : Set α<VAR>H : P ∈ FiniteInter.finiteInterClosure (insert A S)<GOAL>P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>h : ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S<GOAL>FiniteInter (insert Set.univ S)
<VAR>α : Type u<VAR>a : α<GOAL>Function.Injective (List.cons a)
<VAR>α : Type u<GOAL>Function.Injective fun a => [a]
<VAR>α : Type u<VAR>a b : α<GOAL>[a] = [b] ↔ a = b
<VAR>α : Type u<VAR>l : List α<VAR>a : α<GOAL>{x | x ∈ a :: l} = insert a {x | x ∈ l}
<VAR>α : Type u<VAR>DecidableEq α<VAR>a b : α<VAR>l : List α<VAR>h : a ∈ b :: l<GOAL>a = b ∨ a ≠ b ∧ a ∈ l
<VAR>α : Type u<VAR>a b c : α<GOAL>a ∈ [b, c] ↔ a = b ∨ a = c
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>H : Function.Injective f<VAR>a : α<VAR>l : List α<GOAL>f a ∈ List.map f l ↔ a ∈ l
<VAR>α : Type u<VAR>f : α → α<VAR>hf : Function.Involutive f<VAR>x : α<VAR>l : List α<GOAL>(∃ y, y ∈ l ∧ f y = x) ↔ f x ∈ l
<VAR>α : Type u<VAR>f : α → α<VAR>hf : Function.Involutive f<VAR>a : α<VAR>l : List α<GOAL>a ∈ List.map f l ↔ f a ∈ l
<VAR>α : Type u<VAR>l : List α<GOAL>0 < l.length ↔ l ≠ []
<VAR>α : Type u<VAR>n : ℕ<VAR>l : List α<GOAL>l.length = n + 1 → ∃ h t, l = h :: t
<VAR>α : Type u<GOAL>Function.Injective List.length ↔ Subsingleton α
<VAR>α : Type u<VAR>Subsingleton α<GOAL>Function.Injective List.length
<VAR>α : Type u<VAR>l : List α<GOAL>l.length = 2 ↔ ∃ a b, l = [a, b]
<VAR>α : Type u<VAR>l : List α<GOAL>l.length = 3 ↔ ∃ a b c, l = [a, b, c]
<VAR>α : Type u<VAR>x : α<GOAL>{x} = [x]
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : α<VAR>l : List α<VAR>h : ¬x ∈ l<GOAL>insert x l = x :: l
<VAR>α : Type u<VAR>DecidableEq α<VAR>x : α<VAR>l : List α<VAR>h : x ∈ l<GOAL>insert x l = l
<VAR>α : Type u<VAR>DecidableEq α<VAR>x y : α<VAR>h : x ≠ y<GOAL>{x, y} = [x, y]
<VAR>α : Type u<VAR>p : α → Prop<VAR>a : α<VAR>l : List α<VAR>h : ∀ (x : α), x ∈ a :: l → p x<VAR>x : α<GOAL>x ∈ l → p x
<VAR>α : Type u<VAR>p : α → Prop<VAR>a : α<VAR>l : List α<VAR>h : p a<GOAL>∃ x, x ∈ a :: l ∧ p x
<VAR>α : Type u<VAR>p : α → Prop<VAR>a : α<VAR>l : List α<GOAL>(∃ x, x ∈ l ∧ p x) → ∃ x, x ∈ a :: l ∧ p x
<VAR>α : Type u<VAR>p : α → Prop<VAR>a : α<VAR>l : List α<GOAL>(∃ x, x ∈ a :: l ∧ p x) → p a ∨ ∃ x, x ∈ l ∧ p x
<VAR>α : Type u<VAR>p : α → Prop<VAR>a : α<VAR>l : List α<GOAL>(∃ x, x ∈ a :: l ∧ p x) ↔ p a ∨ ∃ x, x ∈ l ∧ p x
<VAR>α : Type u<VAR>a : α<VAR>l m : List α<VAR>ainm : a ∈ m<VAR>lsubm : l ⊆ m<GOAL>a :: l ⊆ m
<VAR>α : Type u<VAR>l₁ l₂ l : List α<VAR>l₁subl : l₁ ⊆ l<VAR>l₂subl : l₂ ⊆ l<GOAL>l₁ ++ l₂ ⊆ l
<VAR>α : Type u<VAR>β : Type v<VAR>l₁ l₂ : List α<VAR>f : α → β<VAR>h : Function.Injective f<GOAL>List.map f l₁ ⊆ List.map f l₂ ↔ l₁ ⊆ l₂
<VAR>α : Type u<VAR>L₁ L₂ : List α<GOAL>L₁.append L₂ = L₁ ++ L₂
<VAR>α : Type u<VAR>x y : List α<GOAL>x ++ y = y ↔ x = []
<VAR>α : Type u<VAR>x y : List α<GOAL>y = x ++ y ↔ x = []
<VAR>α : Type u<VAR>x y : List α<GOAL>x ++ y = x ↔ y = []
<VAR>α : Type u<VAR>x y : List α<GOAL>x = x ++ y ↔ y = []
<VAR>α : Type u<VAR>s : List α<GOAL>Function.Injective fun t => s ++ t
<VAR>α : Type u<VAR>t : List α<GOAL>Function.Injective fun s => s ++ t
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>l = List.replicate l.length a ↔ ∀ (b : α), b ∈ l → b = a
<VAR>α : Type u<VAR>m n : ℕ<VAR>a : α<GOAL>List.replicate (m + n) a = List.replicate m a ++ List.replicate n a
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<GOAL>List.replicate (n + 1) a = List.replicate n a ++ [a]
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<GOAL>List.replicate n a ⊆ [a]
<VAR>α : Type u<VAR>a : α<VAR>L : List α<GOAL>L ⊆ [a] ↔ ∃ n, L = List.replicate n a
<VAR>α : Type u<VAR>a : α<VAR>n : ℕ<GOAL>(List.replicate n a).tail = List.replicate (n - 1) a
<VAR>α : Type u<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Function.Injective (List.replicate n)
<VAR>α : Type u<VAR>a b : α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>List.replicate n a = List.replicate n b ↔ a = b
<VAR>α : Type u<VAR>a b : α<VAR>n : ℕ<GOAL>List.replicate n a = List.replicate n b ↔ n = 0 ∨ a = b
<VAR>α : Type u<VAR>a : α<GOAL>Function.Injective fun x => List.replicate x a
<VAR>α : Type u<VAR>a : α<VAR>n m : ℕ<GOAL>List.replicate n a = List.replicate m a ↔ n = m
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<VAR>h : List.replicate n a ≠ []<GOAL>(List.replicate n a).head h = a
<VAR>α : Type u<VAR>x y : α<GOAL>x ∈ pure y ↔ x = y
<VAR>α β : Type u_2<VAR>f : α → List β<VAR>l : List α<GOAL>l >>= f = l.bind f
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(a :: l).reverse = l.reverse.concat a
<VAR>α : Type u<VAR>l : List α<VAR>a : α<GOAL>(l ++ [a]).reverse = a :: l.reverse
<VAR>α : Type u<VAR>a : α<GOAL>[a].reverse = [a]
<VAR>α : Type u<GOAL>Function.Involutive List.reverse
<VAR>α : Type u<GOAL>Function.Surjective List.reverse
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>l₁.reverse = l₂.reverse ↔ l₁ = l₂
<VAR>α : Type u<VAR>l l' : List α<GOAL>l.reverse = l' ↔ l = l'.reverse
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>l.concat a = (a :: l.reverse).reverse
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l₁ l₂ : List α<GOAL>List.map f (l₁.reverseAux l₂) = (List.map f l₁).reverseAux (List.map f l₂)
<VAR>α : Type u<VAR>l : List α<GOAL>l.isEmpty = true ↔ l = []
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>h : l ≠ []<GOAL>(a :: l).getLast ⋯ = l.getLast h
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(l ++ [a]).getLast ⋯ = a
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>h : l₂ ≠ []<GOAL>(l₁ ++ l₂).getLast ⋯ = l₂.getLast h
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(l.concat a).getLast ⋯ = a
<VAR>α : Type u<VAR>a : α<GOAL>[a].getLast ⋯ = a
<VAR>α : Type u<VAR>a₁ a₂ : α<VAR>l : List α<GOAL>(a₁ :: a₂ :: l).getLast ⋯ = (a₂ :: l).getLast ⋯
<VAR>α : Type u<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.dropLast ++ [l.getLast h] = l
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>h₁ : l₁ ≠ []<VAR>h₂ : l₂ ≠ []<VAR>h₃ : l₁ = l₂<GOAL>l₁.getLast h₁ = l₂.getLast h₂
<VAR>α : Type u<VAR>m : ℕ<VAR>a : α<GOAL>(List.replicate (m + 1) a).getLast ⋯ = a
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<VAR>hlp : List.filter p l ≠ []<GOAL>p (l.getLast ⋯) = true → (List.filter p l).getLast hlp = l.getLast ⋯
<VAR>α : Type u<VAR>a b : α<VAR>l : List α<GOAL>(a :: b :: l).getLast? = (b :: l).getLast?
<VAR>α : Type u<VAR>l : List α<GOAL>l.getLast? = none ↔ l = []
<VAR>α : Type u<VAR>l : List α<GOAL>l.getLast?.isSome = true ↔ l ≠ []
<VAR>α : Type u<VAR>l : List α<VAR>x : α<GOAL>x ∈ l.getLast? → ∃ h, x = l.getLast h
<VAR>α : Type u<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.getLast? = some (l.getLast h)
<VAR>α : Type u<VAR>x y : α<VAR>l : List α<GOAL>x ∈ l.getLast? → x ∈ (y :: l).getLast?
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>ha : a ∈ l.getLast?<GOAL>a ∈ l
<VAR>α : Type u<VAR>l : List α<VAR>a : α<GOAL>a ∈ l.getLast? → l.dropLast ++ [a] = l
<VAR>α : Type u<VAR>Inhabited α<VAR>l : List α<GOAL>l.getLastI = l.getLast?.iget
<VAR>α : Type u<VAR>l₁ : List α<VAR>a : α<VAR>l₂ : List α<GOAL>(l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
<VAR>α : Type u<VAR>l₁ : List α<VAR>l₂ : List α<GOAL>l₂ ≠ [] → (l₁ ++ l₂).getLast? = l₂.getLast?
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>x : α<VAR>h : x ∈ l₂.getLast?<GOAL>x ∈ (l₁ ++ l₂).getLast?
<VAR>α : Type u<VAR>Inhabited α<GOAL>[].head! = default
<VAR>α : Type u<VAR>x : List α<VAR>h : x ≠ []<GOAL>x.head h :: x.tail = x
<VAR>α : Type u<VAR>Inhabited α<VAR>l : List α<GOAL>l.head! = l.head?.iget
<VAR>α : Type u<VAR>Inhabited α<GOAL>Function.Surjective List.head!
<VAR>α : Type u<GOAL>Function.Surjective List.head?
<VAR>α : Type u<GOAL>Function.Surjective List.tail
<VAR>α : Type u<VAR>x : α<VAR>l : List α<GOAL>x ∈ l.head? → l = x :: l.tail
<VAR>α : Type u<VAR>x : α<VAR>l : List α<VAR>h : x ∈ l.head?<GOAL>x ∈ l
<VAR>α : Type u<VAR>Inhabited α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).head! = a
<VAR>α : Type u<VAR>Inhabited α<VAR>t : List α<VAR>s : List α<VAR>h : s ≠ []<GOAL>(s ++ t).head! = s.head!
<VAR>α : Type u<VAR>s t : List α<VAR>x : α<VAR>h : x ∈ s.head?<GOAL>x ∈ (s ++ t).head?
<VAR>α : Type u<VAR>l₁ : List α<VAR>l₂ : List α<GOAL>l₁ ≠ [] → (l₁ ++ l₂).head? = l₁.head?
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>h : l ≠ []<GOAL>(l ++ [a]).tail = l.tail ++ [a]
<VAR>α : Type u<VAR>l : List α<VAR>a : α<GOAL>a ∈ l.head? → a :: l.tail = l
<VAR>α : Type u<VAR>Inhabited α<VAR>l : List α<GOAL>l ≠ [] → l.head! ∈ l.head?
<VAR>α : Type u<VAR>Inhabited α<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.head! :: l.tail = l
<VAR>α : Type u<VAR>Inhabited α<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.head! ∈ l
<VAR>α : Type u<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.head h ∈ l
<VAR>α : Type u<VAR>l l' : List α<VAR>h : l ≠ []<GOAL>(l ++ l').tail = l.tail ++ l'
<VAR>α : Type u<VAR>l : List α<VAR>i : ℕ<VAR>h : i < l.length<GOAL>l[i] = l[i]?.get ⋯
<VAR>α : Type u<VAR>l : List α<VAR>i : Fin l.length<GOAL>l.get i = (l.get? ↑i).get ⋯
<VAR>α : Type u<VAR>l : List α<VAR>i : ℕ<VAR>h : i < l.tail.length<VAR>h' : i + 1 < l.length := ⋯<GOAL>l.tail.nthLe i h = l.nthLe (i + 1) h'
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : n < (a :: l).length<GOAL>n - 1 < l.length
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>n : ℕ<VAR>hl : n < (a :: l).length<GOAL>(a :: l).nthLe n hl = if hn : n = 0 then a else l.nthLe (n - 1) ⋯
<VAR>α : Type u<VAR>l : List α<VAR>f g : α → α<GOAL>List.modifyHead g (List.modifyHead f l) = List.modifyHead (g ∘ f) l
<VAR>α : Type u<VAR>motive : List α → Sort u_2<VAR>nil : motive []<VAR>append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])<GOAL>List.reverseRecOn [] nil append_singleton = nil
<VAR>α : Type u<VAR>motive : List α → Sort u_2<VAR>x : α<VAR>xs : List α<VAR>nil : motive []<VAR>append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])<GOAL>List.reverseRecOn (xs ++ [x]) nil append_singleton = append_singleton xs x (List.reverseRecOn xs nil append_singleton)
<VAR>α : Type u<VAR>motive : List α → Sort u_2<VAR>nil : motive []<VAR>singleton : (a : α) → motive [a]<VAR>cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))<GOAL>List.bidirectionalRec nil singleton cons_append [] = nil
<VAR>α : Type u<VAR>motive : List α → Sort u_2<VAR>nil : motive []<VAR>singleton : (a : α) → motive [a]<VAR>cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))<VAR>a : α<GOAL>List.bidirectionalRec nil singleton cons_append [a] = singleton a
<VAR>α : Type u<VAR>motive : List α → Sort u_2<VAR>nil : motive []<VAR>singleton : (a : α) → motive [a]<VAR>cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))<VAR>a : α<VAR>l : List α<VAR>b : α<GOAL>List.bidirectionalRec nil singleton cons_append (a :: (l ++ [b])) = cons_append a l b (List.bidirectionalRec nil singleton cons_append l)
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>a : α<VAR>s : l₁.Sublist l₂<GOAL>(a :: l₁).Sublist (a :: l₂)
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>a b : α<GOAL>(a :: l₁).Sublist (b :: l₂) ↔ (a :: l₁).Sublist l₂ ∨ a = b ∧ l₁.Sublist l₂
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>a : α<VAR>h : l₁.Sublist l₂<GOAL>l₁.Sublist (a :: l₂)
<VAR>α : Type u<VAR>l : List α<GOAL>l.tail.Sublist l
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>l₁.Sublist l₂ → l₁.tail.Sublist l₂.tail
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>a b : α<VAR>h : (a :: l₁).Sublist (b :: l₂)<GOAL>l₁.Sublist l₂
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>a : α<VAR>h : (a :: l₁).Sublist (a :: l₂)<GOAL>l₁.Sublist l₂
<VAR>α : Type u<VAR>l : List α<VAR>s : l.Sublist []<GOAL>l = []
<VAR>α : Type u<VAR>l : List α<VAR>a : α<GOAL>l.Sublist [a] ↔ l = [] ∨ l = [a]
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>n : ℕ<GOAL>l.Sublist (List.replicate n a) ↔ ∃ k, k ≤ n ∧ l = List.replicate k a
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>s₁ : l₁.Sublist l₂<VAR>s₂ : l₂.Sublist l₁<GOAL>l₁ = l₂
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>List.indexOf a (a :: l) = 0
<VAR>α : Type u<VAR>DecidableEq α<VAR>a b : α<VAR>l : List α<GOAL>b = a → List.indexOf a (b :: l) = 0
<VAR>α : Type u<VAR>DecidableEq α<VAR>a b : α<VAR>l : List α<GOAL>b ≠ a → List.indexOf a (b :: l) = (List.indexOf a l).succ
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>List.indexOf a l = l.length ↔ ¬a ∈ l
<VAR>α : Type u<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>¬a ∈ l → List.indexOf a l = l.length
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>List.indexOf a l ≤ l.length
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>List.indexOf a l < l.length ↔ a ∈ l
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>DecidableEq α<VAR>a : α<VAR>h : a ∈ l₁<GOAL>List.indexOf a (l₁ ++ l₂) = List.indexOf a l₁
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>DecidableEq α<VAR>a : α<VAR>h : ¬a ∈ l₁<GOAL>List.indexOf a (l₁ ++ l₂) = l₁.length + List.indexOf a l₂
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>∃ n h, l.nthLe n h = a
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>h : n < l.length<GOAL>l.get? n = some (l.nthLe n h)
<VAR>α : Type u<VAR>l : List α<GOAL>l[l.length]? = none
<VAR>α : Type u<VAR>l : List α<GOAL>l.get? l.length = none
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>h : n < l.length<GOAL>l.nthLe n h ∈ l
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>a ∈ l ↔ ∃ n h, l.nthLe n h = a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<VAR>n : ℕ<VAR>H1 : n < (List.map f l).length<VAR>H2 : n < l.length<GOAL>(List.map f l).nthLe n H1 = f (l.nthLe n H2)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<VAR>n : ℕ<VAR>h : n < l.length<GOAL>f l[n] = (List.map f l)[n]
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<VAR>n : Fin l.length<GOAL>f (l.get n) = (List.map f l).get ⟨↑n, ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<VAR>n : ℕ<VAR>H : n < l.length<GOAL>f (l.nthLe n H) = (List.map f l).nthLe n ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<VAR>n : ℕ<VAR>H : n < (List.map f l).length<GOAL>(List.map f l).nthLe n H = f (l.nthLe n ⋯)
<VAR>α : Type u<VAR>a : α<VAR>n : ℕ<VAR>hn : n < 1<GOAL>[a].nthLe n hn = a
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>n : ℕ<VAR>h₁ : l₁.length ≤ n<VAR>h₂ : n < (l₁ ++ l₂).length<GOAL>(l₁ ++ l₂).nthLe n h₂ = l₂.nthLe (n - l₁.length) ⋯
<VAR>α : Type u<VAR>l : List α<VAR>h : l.length - 1 < l.length<GOAL>l.get ⟨l.length - 1, h⟩ = l.getLast ⋯
<VAR>α : Type u<VAR>x : α<VAR>xs : List α<VAR>n : ℕ<VAR>h : n = xs.length<GOAL>(x :: xs).nthLe n ⋯ = (x :: xs).getLast ⋯
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>h : n < l.length<GOAL>List.take 1 (List.drop n l) = [l.get ⟨n, h⟩]
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>h' : ∀ (n : ℕ), n < max l₁.length l₂.length → l₁.get? n = l₂.get? n<GOAL>l₁ = l₂
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>l₁ = l₂ ↔ ∀ (n : ℕ), l₁.get? n = l₂.get? n
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>l₁ = l₂ ↔ ∀ (n : ℕ), n < max l₁.length l₂.length → l₁.get? n = l₂.get? n
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>hl : l₁.length = l₂.length<VAR>h : ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.nthLe n h₁ = l₂.nthLe n h₂<GOAL>l₁ = l₂
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : List.indexOf a l < l.length<GOAL>l[List.indexOf a l] = a
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : List.indexOf a l < l.length<GOAL>l.get ⟨List.indexOf a l, h⟩ = a
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>l[List.indexOf a l]? = some a
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>l.get? (List.indexOf a l) = some a
<VAR>α : Type u<VAR>l r : List α<VAR>i : ℕ<VAR>h1 : i + l.length < (l.reverseAux r).length<VAR>h2 : i < r.length<GOAL>(l.reverseAux r).get ⟨i + l.length, h1⟩ = r.get ⟨i, h2⟩
<VAR>α : Type u<VAR>DecidableEq α<VAR>l : List α<VAR>x y : α<VAR>hx : x ∈ l<VAR>hy : y ∈ l<GOAL>List.indexOf x l = List.indexOf y l ↔ x = y
<VAR>α : Type u<VAR>l r : List α<VAR>i : ℕ<VAR>h1 : l.length - 1 - i < (l.reverseAux r).length<VAR>h2 : i < l.length<GOAL>(l.reverseAux r)[l.length - 1 - i] = l[i]
<VAR>α : Type u<VAR>l : List α<VAR>i : ℕ<VAR>h1 : l.length - 1 - i < l.reverse.length<VAR>h2 : i < l.length<GOAL>l.reverse[l.length - 1 - i] = l[i]
<VAR>α : Type u<VAR>l r : List α<VAR>i : ℕ<VAR>h1 : l.length - 1 - i < (l.reverseAux r).length<VAR>h2 : i < l.length<GOAL>(l.reverseAux r).get ⟨l.length - 1 - i, h1⟩ = l.get ⟨i, h2⟩
<VAR>α : Type u<VAR>l : List α<VAR>i : ℕ<VAR>h1 : l.length - 1 - i < l.reverse.length<VAR>h2 : i < l.length<GOAL>l.reverse.get ⟨l.length - 1 - i, h1⟩ = l.get ⟨i, h2⟩
<VAR>α : Type u<VAR>l : List α<VAR>i : ℕ<VAR>h1 : l.length - 1 - i < l.reverse.length<VAR>h2 : i < l.length<GOAL>l.reverse.nthLe (l.length - 1 - i) h1 = l.nthLe i h2
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>hn : n < l.reverse.length<VAR>hn' : l.length - 1 - n < l.length<GOAL>l.reverse.nthLe n hn = l.nthLe (l.length - 1 - n) hn'
<VAR>α : Type u<VAR>l : List α<VAR>n : Fin l.reverse.length<VAR>hn' : l.length - 1 - ↑n < l.length<GOAL>l.reverse.get n = l.get ⟨l.length - 1 - ↑n, hn'⟩
<VAR>α : Type u<VAR>l : List α<VAR>h : l.length = 1<GOAL>l = [l.nthLe 0 ⋯]
<VAR>α : Type u<VAR>f g : List α → List α<VAR>m n : ℕ<VAR>l : List α<GOAL>List.modifyNthTail g (m + n) (List.modifyNthTail f n l) = List.modifyNthTail (fun l => List.modifyNthTail g m (f l)) n l
<VAR>α : Type u<VAR>f g : List α → List α<VAR>m n : ℕ<VAR>l : List α<VAR>h : n ≤ m<GOAL>List.modifyNthTail g m (List.modifyNthTail f n l) = List.modifyNthTail (fun l => List.modifyNthTail g (m - n) (f l)) n l
<VAR>α : Type u<VAR>f g : List α → List α<VAR>n : ℕ<VAR>l : List α<GOAL>List.modifyNthTail g n (List.modifyNthTail f n l) = List.modifyNthTail (g ∘ f) n l
<VAR>α : Type u<VAR>f : α → α<VAR>n : ℕ<VAR>l : List α<GOAL>List.modifyNth f n l = ((fun a => l.set n (f a)) <$> l[n]?).getD l
<VAR>α : Type u<VAR>f : List α → List α<VAR>H : ∀ (l : List α), (f l).length = l.length<VAR>n : ℕ<VAR>l : List α<GOAL>(List.modifyNthTail f n l).length = l.length
<VAR>α : Type u<VAR>f : α → α<VAR>n : ℕ<VAR>l : List α<GOAL>(List.modifyNth f n l).length = l.length
<VAR>α : Type u<VAR>l : List α<VAR>i j : ℕ<VAR>h : i ≠ j<VAR>a : α<VAR>hj : j < (l.set i a).length<GOAL>(l.set i a)[j] = l[j]
<VAR>α : Type u<VAR>l : List α<VAR>i j : ℕ<VAR>h : i ≠ j<VAR>a : α<VAR>hj : j < (l.set i a).length<GOAL>(l.set i a).get ⟨j, hj⟩ = l.get ⟨j, ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<GOAL>l.bind (pure ∘ f) = List.map f l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<GOAL>l.bind (List.ret ∘ f) = List.map f l
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f g : α → List β<VAR>h : ∀ (x : α), x ∈ l → f x = g x<GOAL>l.bind f = l.bind g
<VAR>α : Type u<VAR>a : α<VAR>as : List α<VAR>h : a ∈ as<VAR>f : α → List α<GOAL>f a <:+: as.bind f
<VAR>α β : Type u_2<VAR>f : α → β<VAR>l : List α<GOAL>f <$> l = List.map f l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<GOAL>List.map f l.tail = (List.map f l).tail
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>h : β → γ<VAR>g : α → β<VAR>l : List α<GOAL>List.map (h ∘ g) l = List.map h (List.map g l)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>g : β → γ<VAR>f : α → β<GOAL>List.map g ∘ List.map f = List.map (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse f g<GOAL>Function.LeftInverse (List.map f) (List.map g)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.RightInverse f g<GOAL>Function.RightInverse (List.map f) (List.map g)
<VAR>α : Type u<VAR>f : α → α<VAR>h : Function.Involutive f<GOAL>Function.Involutive (List.map f)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<GOAL>Function.LeftInverse (List.map f) (List.map g) ↔ Function.LeftInverse f g
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<GOAL>Function.RightInverse (List.map f) (List.map g) ↔ Function.RightInverse f g
<VAR>α : Type u<VAR>f : α → α<GOAL>Function.Involutive (List.map f) ↔ Function.Involutive f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Function.Injective f<GOAL>Function.Injective (List.map f)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Function.Injective (List.map f) ↔ Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Function.Surjective f<GOAL>Function.Surjective (List.map f)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Function.Surjective (List.map f) ↔ Function.Surjective f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Function.Bijective f<GOAL>Function.Bijective (List.map f)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Function.Bijective (List.map f) ↔ Function.Bijective f
<VAR>α : Type u<VAR>β : Type v<VAR>b₁ b₂ : β<VAR>l : List α<VAR>h : b₁ ∈ List.map (Function.const α b₂) l<GOAL>b₁ = b₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β → γ<VAR>l : List β<GOAL>List.zipWith f [] l = []
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β → γ<VAR>l : List α<GOAL>List.zipWith f l [] = []
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β → γ<VAR>as : List α<VAR>bs : List β<GOAL>List.zipWith (flip f) bs as = List.zipWith f as bs
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<VAR>l : List α<GOAL>List.take n.succ (a :: l) = a :: List.take n l
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>List.drop n l.tail = List.drop (n + 1) l
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>h : n < l.length<GOAL>l[n] :: List.drop (n + 1) l = List.drop n l
<VAR>α : Type u<VAR>l : List α<VAR>n : Fin l.length<GOAL>l.get n :: List.drop (↑n + 1) l = List.drop (↑n) l
<VAR>α : Type u<VAR>Inhabited α<VAR>n : ℕ<VAR>l : List α<GOAL>(List.takeI n l).length = n
<VAR>α : Type u<VAR>Inhabited α<VAR>n : ℕ<GOAL>List.takeI n [] = List.replicate n default
<VAR>α : Type u<VAR>Inhabited α<VAR>n : ℕ<VAR>l : List α<GOAL>n ≤ l.length → List.takeI n l = List.take n l
<VAR>α : Type u<VAR>Inhabited α<VAR>l₁ l₂ : List α<GOAL>List.takeI l₁.length (l₁ ++ l₂) = l₁
<VAR>α : Type u<VAR>Inhabited α<VAR>l₁ l₂ : List α<VAR>n : ℕ<VAR>h : l₁.length = n<GOAL>List.takeI n (l₁ ++ l₂) = l₁
<VAR>α : Type u<VAR>n : ℕ<VAR>l : List α<VAR>a : α<GOAL>(List.takeD n l a).length = n
<VAR>α : Type u<VAR>n : ℕ<VAR>l : List α<VAR>a : α<GOAL>n ≤ l.length → List.takeD n l a = List.take n l
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>a : α<GOAL>List.takeD l₁.length (l₁ ++ l₂) a = l₁
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>n : ℕ<VAR>a : α<VAR>h : l₁.length = n<GOAL>List.takeD n (l₁ ++ l₂) a = l₁
<VAR>α : Type u<VAR>β : Type v<VAR>f g : α → β → α<VAR>a : α<VAR>l : List β<VAR>H : ∀ (a : α) (b : β), b ∈ l → f a b = g a b<GOAL>List.foldl f a l = List.foldl g a l
<VAR>α : Type u<VAR>β : Type v<VAR>f g : α → β → β<VAR>b : β<VAR>l : List α<VAR>H : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b<GOAL>List.foldr f b l = List.foldr g b l
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α → β<VAR>b : β<VAR>x : α<VAR>xs : List α<GOAL>List.foldl f b (xs ++ [x]) = f (List.foldl f b xs) x
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β → β<VAR>b : β<VAR>x : α<VAR>xs : List α<GOAL>List.foldr f b (xs ++ [x]) = List.foldr f (f x b) xs
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β → α<VAR>a : α<VAR>hf : ∀ (b : β), f a b = a<VAR>l : List β<GOAL>List.foldl f a l = a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β → β<VAR>b : β<VAR>hf : ∀ (a : α), f a b = b<VAR>l : List α<GOAL>List.foldr f b l = b
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>l : List β<GOAL>List.foldl (fun a x => a) a l = a
<VAR>α : Type u<VAR>β : Type v<VAR>b : β<VAR>l : List α<GOAL>List.foldr (fun x b => b) b l = b